ref.mlw 907 Bytes
Newer Older
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
1

MARCHE Claude's avatar
MARCHE Claude committed
2
(** {1 References}
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
3

4
   A mutable variable, or "reference" in ML terminology, is simply a
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7 8 9 10 11
   record with a single mutable field [contents].
*)

(** {2 Generic references}

   Creation, access, and assignment are provided as [ref], prefix [!], and
   infix [:=], respectively.
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
12
*)
13 14 15

module Ref

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 23

end

MARCHE Claude's avatar
MARCHE Claude committed
24 25 26
(** {2 Integer References}

a few operations specific to integer references *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
27

28 29
module Refint

30
  use int.Int
31
  use export Ref
32

33 34
  let incr (ref r: int) ensures { r = old r + 1 } = r <- r + 1
  let decr (ref r: int) ensures { r = old r - 1 } = r <- r - 1
35

36 37 38
  let (+=)   (ref r: int) (v: int) ensures { r = old r + v } = r <- r + v
  let (-=)   (ref r: int) (v: int) ensures { r = old r - v } = r <- r - v
  let ( *= ) (ref r: int) (v: int) ensures { r = old r * v } = r <- r * v
39 40

end