diff --git a/examples/bignum.mlw b/examples/bignum.mlw index 7a5585ed16b8ef49358b07e7d777b5baccb1cd66..c7cb2a07cec7853ed21927287cdf06d7f95c0b6c 100644 --- a/examples/bignum.mlw +++ b/examples/bignum.mlw @@ -13,8 +13,8 @@ module BigNum use import int.Int use import list.List - constant base: int - axiom base_gt1: base > 1 + val constant base: int + ensures { result > 1 } type digit = int type num = list digit diff --git a/examples/binomial_heap.mlw b/examples/binomial_heap.mlw index e60731f48edaf6880f8cff082b220dde07382022..6dcf4c92e853879c9fda1461629957a172d8c899 100644 --- a/examples/binomial_heap.mlw +++ b/examples/binomial_heap.mlw @@ -19,7 +19,7 @@ module BinomialHeap type elt - predicate le elt elt + val predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le (** Trees. @@ -168,8 +168,7 @@ module BinomialHeap let is_empty (h: heap) : bool ensures { result <-> h = Nil } - = - h = Nil + = match h with Nil -> true | _ -> false end let get_min (h: heap) : elt requires { heaps h } @@ -193,7 +192,7 @@ module BinomialHeap aux t.elem l end - function link (t1 t2: tree) : tree = + let function link (t1 t2: tree) : tree = if le t1.elem t2.elem then { elem = t1.elem; rank = t1.rank + 1; children = Cons t2 t1.children } else diff --git a/examples/coincidence_count_list.mlw b/examples/coincidence_count_list.mlw index a21037d1a942dce90251f658c76c1ef395831f4f..80036b1378c9d91fafc0cb30a0851f27619c2def 100644 --- a/examples/coincidence_count_list.mlw +++ b/examples/coincidence_count_list.mlw @@ -54,7 +54,13 @@ module CoincidenceCountAnyType use list.Mem as L use import int.Int - clone import relations.TotalStrictOrder + type t + + val predicate eq (x y : t) + ensures { result <-> x = y } + val predicate rel (x y : t) + + clone import relations.TotalStrictOrder with type t, predicate rel clone export list.Sorted with type t = t, predicate le = rel, goal Transitive.Trans @@ -67,7 +73,7 @@ module CoincidenceCountAnyType = match a, b with | Cons ha ta, Cons hb tb -> - if ha = hb then + if eq ha hb then add ha (coincidence_count ta tb) else if rel ha hb then coincidence_count ta b diff --git a/examples/esterel.mlw b/examples/esterel.mlw index f36c5325878ecb179e3e76ce68f0c84c0639fa47..ea98ed1170b48b45f24f92033a3c99193e3a29ef 100644 --- a/examples/esterel.mlw +++ b/examples/esterel.mlw @@ -33,7 +33,7 @@ module Esterel ghost mdl: set int; (* its interpretation as a set *) } invariant { - forall i: int. (0 <= i < size /\ nth self.bv i) <-> mem i self.mdl + forall i: int. (0 <= i < size /\ nth bv i) <-> mem i mdl } diff --git a/examples/koda_ruskey.mlw b/examples/koda_ruskey.mlw index 3c6d8f3abbb4b5314f097016d2bfde9969adba77..ef54d76b449743a3545e976b37bc502edda55eac 100644 --- a/examples/koda_ruskey.mlw +++ b/examples/koda_ruskey.mlw @@ -441,42 +441,47 @@ module KodaRuskey assert { not (mem_stack i st') }; let ghost visited1 = !visited in if bits[i] = White then begin - 'A: enum bits f0 (Cons f2 st'); + label A in + enum bits f0 (Cons f2 st'); assert { sub st f0 bits.elts }; let ghost bits1 = map_of_array bits in let ghost visited2 = !visited in - 'B: bits[i] <- Black; + label B in + bits[i] <- Black; assert { sub st f0 bits.elts }; assert { white_forest f1 bits.elts }; - assert { unchanged (Cons f2 st') (at bits 'B).elts bits.elts}; - assert { inverse (Cons f2 st') (at bits 'A).elts bits.elts }; - 'C: enum bits f0 (Cons f1 (Cons f2 st')); + assert { unchanged (Cons f2 st') (bits at B).elts bits.elts}; + assert { inverse (Cons f2 st') (bits at A).elts bits.elts }; + label C in + enum bits f0 (Cons f1 (Cons f2 st')); assert { bits[i] = Black }; assert { final_forest f1 bits.elts }; assert { if not (even_forest f1) - then inverse (Cons f2 st') (at bits 'C).elts bits.elts && + then inverse (Cons f2 st') (bits at C).elts bits.elts && white_forest f2 bits.elts - else unchanged (Cons f2 st') (at bits 'C).elts bits.elts && + else unchanged (Cons f2 st') (bits at C).elts bits.elts && final_forest f2 bits.elts }; ghost stored_trans1 f0 bits1 (map_of_array bits) i f1 f2 st' visited1 visited2 !visited end else begin assert { if not (even_forest f1) then white_forest f2 bits.elts else final_forest f2 bits.elts }; - 'A: enum bits f0 (Cons f1 (Cons f2 st')); + label A in + enum bits f0 (Cons f1 (Cons f2 st')); assert { sub st f0 bits.elts }; let ghost bits1 = map_of_array bits in let ghost visited2 = !visited in - 'B: bits[i] <- White; + label B in + bits[i] <- White; assert { unchanged (Cons f1 (Cons f2 st')) - (at bits 'B).elts bits.elts }; + (bits at B).elts bits.elts }; assert { inverse (Cons f1 (Cons f2 st')) - (at bits 'A).elts bits.elts }; + (bits at A).elts bits.elts }; assert { sub st f0 bits.elts }; assert { if even_forest f1 || even_forest f2 - then unchanged st' (at bits 'A).elts bits.elts - else inverse st' (at bits 'A).elts bits.elts }; - 'C: enum bits f0 (Cons f2 st'); + then unchanged st' (bits at A).elts bits.elts + else inverse st' (bits at A).elts bits.elts }; + enum bits f0 (Cons f2 st'); assert { bits[i] = White }; assert { white_forest f bits.elts }; ghost stored_trans2 f0 bits1 (map_of_array bits) diff --git a/examples/power.mlw b/examples/power.mlw index 741112f6a562a0aa7cefddffc1074ccd037edb42..7b6a5db28b674a7e8a7dfa934644b64d710501e7 100644 --- a/examples/power.mlw +++ b/examples/power.mlw @@ -32,12 +32,12 @@ module FastExponentiation while !e > 0 do invariant { 0 <= !e /\ !r * power !p !e = power x n } variant { !e } - 'L: + label L in if mod !e 2 = 1 then r := !r * !p; p := !p * !p; e := div !e 2; assert { power !p !e = - let x = power (at !p 'L) !e in x * x } + let x = power (!p at L) !e in x * x } done; !r diff --git a/examples/schorr_waite_via_recursion.mlw b/examples/schorr_waite_via_recursion.mlw index 242ba20d7541e91fc0aa87ecd5af525035f21ad8..76850dfcc5d291920bfbe12ece1d41eb23e7b931 100644 --- a/examples/schorr_waite_via_recursion.mlw +++ b/examples/schorr_waite_via_recursion.mlw @@ -42,7 +42,7 @@ module Memory (** Memory blocks have two parts: a marking part containing in particular Schorr-Waite internal management data, and a sequence of pointers to other memory blocks. *) - type memory model { + type memory = abstract { (** Associate block size to location. *) block_size : map loc int; (** Pointers to other memory blocks. *) diff --git a/examples/verifythis_2016_tree_traversal.mlw b/examples/verifythis_2016_tree_traversal.mlw index 7046998ca045b918a11d18f0172b4151e713fd40..f5690d8299b07f06d73385bee5ab4b88b51771d0 100644 --- a/examples/verifythis_2016_tree_traversal.mlw +++ b/examples/verifythis_2016_tree_traversal.mlw @@ -64,11 +64,12 @@ module Memory use import map.Map (** [loc] is the type of memory locations (e.g pointers) *) type loc + val predicate eq (x y:loc) ensures { result <-> x = y } (** Kinds of pointer fields. *) type kind = Parent | Left | Right (** Convenience alias for a pointer field table. *) type pmem = map kind (map loc loc) - type memory model { + type memory = abstract { mutable accessor : pmem; mutable mark : map loc bool; } @@ -109,7 +110,7 @@ module Memory (** Non-deterministic initialization. In the original alorithm, the variable y starts uninitialized. *) type non_det_magic - type non_det model { mutable non_det_field : non_det_magic } + type non_det = abstract { mutable non_det_field : non_det_magic } val non_det : non_det val anyloc () : loc writes { non_det } @@ -214,7 +215,7 @@ module TreeShape = match t with | Empty -> () | Node l _ r -> - if c2 = c then (unicity memo t t0 c p2 p;absurd); + if eq c2 c then (unicity memo t t0 c p2 p;absurd); aux l (memo[Left][c2]) c2; aux r (memo[Right][c2]) c2 end in aux lf (memo[Left][c]) c; aux rg (memo[Right][c]) c @@ -374,13 +375,13 @@ module Recursive let ghost _c = !x in let _lf = get_acc Left !x in let _rg = get_acc Right !x in - let ghost (lf, rg) = match t with + let (lf, rg) = ghost match t with | Empty -> absurd | Node l _ r -> (l, r) end in (ghost not_below mem0 lf rg _c !z); bloc mem0 GoLeft; - let b = abstract ensures { result <-> _lf = null /\ _rg = null } + let b = begin ensures { result <-> _lf = null /\ _rg = null } ensures { result -> lf = Empty /\ rg = Empty } is_null _lf && is_null _rg end in if not b then begin @@ -394,13 +395,13 @@ module Recursive in let ghost mem0 = get_all_accs () in try aux t; - 'I: - loop - invariant { memo = at memo 'I } + label I in + while true do + invariant { memo = (memo at I) } invariant { rotated mem0 memo.accessor Finish !x /\ !entered } variant { 0 } bloc mem0 Finish - end + done with Stop -> (ghost ext_cur mem0 t root (null ())); () end end @@ -645,7 +646,7 @@ module Iterative let ghost st = ref Bottom in ghost opening t t stop stop st; let entered = ref false in (* encode do-while loop. *) - while not(abstract ensures { result <-> !x = null } + while not (begin ensures { result <-> !x = null } !entered && is_null !x end) do (* ==> do { BODY } while(x != null); *) invariant { !x = null -> !entered }