vacid_0 examples: termination

examples/vacid_0_build_maze.mlw

@@ -138,6 +138,9 @@ module BuildMaze
 let build_maze (n:int)
   requires { 1 <= n /\ !num_edges = 0 /\
     forall x y:int. x=y <-> path !graph x y }
+  diverges (* termination is only almost sure,
+              assuming rand is well distributed.
+              See http://toccata.lri.fr/gallery/RandomWalk.en.html *)
   ensures { !num_edges = n*n-1 /\
     forall x y:int. 0 <= x < n*n -> 0 <= y < n*n -> path !graph x y }
   = let u = create (n*n) in

examples/vacid_0_red_black_trees.mlw

@@ -153,6 +153,7 @@ module RedBlackTree
 
   let rec find (t : tree) (k : key) : value
     requires { bst t }
+    variant { t }
     ensures { memt t k result }
     raises { Not_found -> forall v : value. not (memt t k v) }
   = match t with
@@ -244,6 +245,7 @@ module RedBlackTree
 
   let rec insert (t : tree) (k : key) (v : value) : tree
     requires { bst t /\ exists n: int. rbtree n t }
+    variant { t }
     ensures { bst result /\
       (forall n : int. rbtree n t -> almost_rbtree n result /\
          (is_not_red t -> rbtree n result)) /\