vstte'10: imperative version of search_list with a loop

examples/programs/vstte10_inverting.mlw

@@ -12,7 +12,7 @@
     forall i j : int. 0 <= i < n -> 0 <= j < n -> i <> j -> a#i <> a#j
 
   logic surjective (a : array int) (n : int) =
-    forall i : int. 0 <= i < n -> exists j : int. (0 <= j < n and a#j = i)
+    forall i : int [i]. 0 <= i < n -> exists j : int. (0 <= j < n and a#j = i)
 
   logic range (a : array int) (n : int) =
     forall i : int. 0 <= i < n -> 0 <= a#i < n

examples/programs/vstte10_search_list.mlw

@@ -31,6 +31,40 @@ let search_list l =
     (result = length l and no_zero l) }
 
 
+(* imperative version, with a loop *)
+
+{
+  use import list.HdTl
+}
+
+let head (l : list 'a) = 
+  { l <> Nil } 
+  match l with Nil -> absurd | Cons h _ -> h end 
+  { hd l = Some result }
+
+let tail (l : list 'a) = 
+  { l <> Nil } 
+  match l with Nil -> absurd | Cons _ t -> t end 
+  { tl l = Some result }
+
+let search_loop l =
+  {}
+  let i = ref 0 in
+  let s = ref l in
+  while !s <> Nil && head !s <> 0 do
+    invariant { 
+      0 <= !i and !i + length !s = length l and
+      (forall j:int. 0 <= j -> nth j !s = nth (!i + j) l) and
+      forall j:int. 0 <= j < !i -> nth j l <> Some 0 }
+    variant { length !s }
+    i := !i + 1;
+    s := tail !s
+  done;
+  !i
+  { (0 <= result < length l and zero_at l result)
+    or 
+    (result = length l and no_zero l) }
+
 (*
 Local Variables: 
 compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_search_list.gui"

theories/list.why

@@ -43,6 +43,35 @@ theory Nth
 
 end
 
+theory HdTl "head and tail"
+
+  use export List
+  use export option.Option
+
+  logic hd (l : list 'a) : option 'a = match l with
+    | Nil -> None
+    | Cons h _ -> Some h
+  end
+
+  logic tl (l : list 'a) : option (list 'a) = match l with
+    | Nil -> None
+    | Cons _ t -> Some t
+  end
+
+  (* TODO: move these lemmas into another theory? *)
+  use import Nth
+  use import int.Int
+
+  lemma Nth_tl :
+    forall l1 l2 : list 'a. tl l1 = Some l2 -> 
+    forall i : int. nth i l2 = nth (i+1) l1
+
+  lemma Nth0_head:
+    forall l : list 'a. nth 0 l = hd l
+
+end
+
+
 theory Append
   use export List