vstte'10 competition : problem 3 in progress (but there seems to be a bug in...

vstte'10 competition : problem 3 in progress (but there seems to be a bug in Why which prevents contructor None to be visible)

examples/programs/.gitignore

 next_digit_sum
 vstte10_max_sum
 vstte10_inverting
+vstte10_search_list

examples/programs/vstte10_search_list.mlw

+(* VSTTE'10 competition 
+   Problem 3: searching a linked list *)
+
+{
+  use export list.List
+  use export list.Length
+  use export option.Option
+
+(*
+  logic nth (n : int) (l : list 'a) = match l with
+   | Nil -> None
+   | Cons x r -> if n = 0 then Some x else nth (n - 1) r
+  end
+*)
+}
+
+let rec search i l = 
+  match l with
+  | Nil -> i
+  | Cons x r -> if x = 0 then i else search (i+1) r
+  end
+
+let search_list l =
+  { }
+  search 0 l
+  { (0 <= result < length l (* nth result l = 0*)) or 
+    (result = length l) }
+
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. examples/programs/vstte10_search_list.gui"
+End: 
+*)

theories/list.why

@@ -29,6 +29,20 @@ theory Mem
 
 end
 
+(*
+theory Nth
+  use export List
+  use import option.Option
+  use import int.Int
+  
+  logic nth (n : int) (l : list 'a) = match l with
+   | Nil -> None
+   | Cons x r -> if n = 0 then Some x else nth (n - 1) r
+  end
+
+end
+*)
+
 theory Sorted
 
   use export List

theories/option.why

+
+theory Option
+
+  type option 'a = None | Some 'a
+
+end