stdlib/ref.mlw

   1
   2 (** {1 References}
   3
   4    A mutable variable, or "reference" in ML terminology, is simply a
   5    record with a single mutable field `contents`.
   6 *)
   7
   8 (** {2 Generic references}
   9
  10    Creation, access, and assignment are provided as `ref`, prefix `!`, and
  11    infix `:=`, respectively.
  12 *)
  13
  14 module Ref
  15
  16   use export why3.Ref.Ref
  17
  18   let function (!) (r: ref 'a) = r.contents
  19
  20   let (:=) (ref r:'a) (v:'a) ensures { r = v } = r <- v
  21
  22 end
  23
  24 (** {2 Integer References}
  25
  26 A few operations specific to integer references. *)
  27
  28 module Refint
  29
  30   use int.Int
  31   use export Ref
  32
  33   let incr (ref r: int) ensures { r = old r + 1 } = r <- r + 1
  34   let decr (ref r: int) ensures { r = old r - 1 } = r <- r - 1
  35
  36   let (+=)   (ref r: int) (v: int) ensures { r = old r + v } = r <- r + v
  37   let (-=)   (ref r: int) (v: int) ensures { r = old r - v } = r <- r - v
  38   let ( *= ) (ref r: int) (v: int) ensures { r = old r * v } = r <- r * v
  39
  40 end