bench and examples programs ported to the new syntax

parent 07c8a484
......@@ -332,6 +332,9 @@ clean::
%.gui: %.why bin/whyide.opt
bin/whyide.opt $*.why
%: %.mlw bin/whyml.opt
bin/whyml.opt $*.mlw
%.gui: %.mlw bin/whyide.opt
bin/whyide.opt $*.mlw
......
module M
let foo (x : ref int) (y : ref int) =
x := 1;
......@@ -7,3 +8,5 @@ parameter r : ref int
let test () =
foo r r
end
module M
let foo (x : ref int) (y : ref int) =
x := 1;
......@@ -6,3 +7,4 @@ let foo (x : ref int) (y : ref int) =
let test (x : ref int) =
foo x x
end
module M
let foo (x : ref int) (y : ref int) =
x := 1;
......@@ -7,3 +8,4 @@ let test () =
let x = ref 0 in
foo x x
end
module M
(* reference would escape its scope *)
let test () =
let x = ref 0 in
fun y -> x := y; !x
end
module M
parameter r : ref (list 'a)
end
module M
(* missing variant *)
let rec even (x:int) : int variant {x} =
odd (x-1)
and odd (x:int) : int =
with odd (x:int) : int =
even (x-1)
end
(* different relations *)
{
module M
logic rel int int
}
let rec even (x:int) : int variant {x} with rel =
odd (x-1)
and odd (x:int) : int variant {x} =
with odd (x:int) : int variant {x} =
even (x-1)
end
module M
parameter incr : x:ref int -> { } unit writes x { !x = old !x + 1 }
use import int.Int
use import module stdlib.Ref
parameter incr : x:ref int -> { } unit writes x { x = old x + 1 }
parameter x : ref int
......@@ -44,9 +48,7 @@ let test_all_1 () =
(* from Cesar Munoz's CD3D *)
{
logic d : int
}
parameter vx : ref int
parameter vy : ref int
......@@ -58,6 +60,7 @@ let test_cd3d () =
if !vx=0 && !vy=0 && sq !vx + sq !vy < sq d then 1 else 2
{ result=1 -> !vx=0 and !vy=0 }
end
(*
Local Variables:
......
module M
exception Exception
parameter f0 : tt:unit ->
......@@ -16,6 +18,8 @@ let f () =
f0 (f1 ())
{ true } | Exception -> { true }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/complex_arg_1"
......
module M
exception Exception of int
parameter t : ref int
......@@ -12,6 +14,7 @@ let test () =
(m ( assert { true } ; 0) 0)
{ true } | Exception -> { true }
end
(*
Local Variables:
......
module M
exception Break
let f (n : int) : int =
......@@ -14,3 +16,6 @@ let f (n : int) : int =
end;
!i
{ result <= 10 }
end
module M
(* exception without argument *)
......@@ -115,6 +116,8 @@ let p16 () = {} if !x = 0 then (x:=1; raise E) { !x<>0 } | E -> { !x=1 }
let p17 () = {} (x := 0; (raise E; x := 1)) { false } | E -> { !x=0 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/exns"
......
module M
(* for loop with invariant *)
let test1 () =
......@@ -78,6 +79,8 @@ let test4d x =
end
{ result=True <-> 0 <= x <= 10 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/for"
......
module M
{
use import list.List
use import list.Length
}
let rec length_ (l : list 'a) variant { length l } =
{}
......@@ -20,6 +19,7 @@ let rec append (l1 : list 'a) (l2 : list 'a) variant { length l1 } =
end
{ length result = length l1 + length l2 }
end
(*
Local Variables:
......
module M
(** 1. A loop increasing [i] up to 10. *)
......@@ -30,6 +31,7 @@ let loop2 (u:unit) =
end
{}
end
(*
Local Variables:
......
module M
{
use import int.EuclideanDivision
logic even (x : int) = x = 2 * (div x 2)
logic odd (x : int) = x = 2 * (div x 2) + 1
}
let rec is_even x : bool variant {x} =
{ 0 <= x }
if x = 0 then True else is_odd (x-1)
{ result=True <-> even x }
and is_odd x : bool variant {x} =
with is_odd x : bool variant {x} =
{ 0 <= x }
if x = 0 then False else is_even (x-1)
{ result=True <-> odd x }
end
(*
Local Variables:
......
module M
{
logic q1 int int int
}
parameter r : ref int
......@@ -10,10 +9,8 @@ parameter f1 : y:int ->
let g1 () = {} f1 !r { q1 (!r) (old (!r)) (old (!r)) }
{
logic foo int : int
logic q int int int
}
parameter f : t:ref int -> x:int ->
{} unit reads t writes t { q (!t) (old (!t)) x }
......@@ -23,6 +20,7 @@ let g (t:ref int) =
f t (foo !t)
{ q (!t) (old (!t)) (foo (old (!t))) }
end
(*
Local Variables:
......
module M
(* Tests for proof obligations. *)
parameter x : ref int
{
logic q(int)
}
logic q int
(* basic stuff: assignment, sequence and local variables *)
......@@ -61,6 +60,8 @@ parameter incrx2 : unit -> { } int writes x { !x = old(!x) + 1 and result = !x }
let p14 () = { !x = 0 } incrx2 () { result = 1 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/po"
......
module M
let f (x:'a) = {} x { result=x }
......@@ -6,6 +7,8 @@ let p () =
if f True then f 1 else f 2
{ result = 1 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/poly"
......
module M
(** Recursive functions *)
......@@ -38,10 +39,10 @@ let rec f5 (a b:ref int) variant { !a } =
let test_f5 () =
{ !x >= 0 } let f = f5 x in let b = ref 0 in f b { result = old !x }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/recfun"
End:
*)
module M
(* Side effect in expressions (Bart Jacobs' tricky example) *)
......@@ -17,6 +18,8 @@ let k () =
end
{ !b1 = 0 and !b2 = 1 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/see"
......
module M
(* side effects in tests *)
......@@ -37,9 +38,10 @@ let p4 (y:ref int) =
done
{ !y = 0 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/set"
End:
*)
module M
parameter x : ref int
......@@ -13,8 +14,11 @@ let p () =
()
end
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/wpcalls"
End:
*)
module M
(* Binary search
......@@ -6,14 +7,12 @@
(* the usual array modeling *)
{
use array.ArrayLength as A
use import int.ComputerDivision
type array = A.t int int
logic (#) (a : array) (i : int) : int = A.get a i
}
let array_get (a : ref array) i =
{ 0 <= i < A.length !a } A.get !a i { result = A.get !a i }
......@@ -55,6 +54,7 @@ let binary_search (a : ref array) (v : int) =
{ 0 <= result < A.length !a and !a#result = v }
| Not_found -> { forall i:int. 0 <= i < A.length !a -> !a#i <> v }
end
(*
Local Variables:
......
module M
(* Bresenham line drawing algorithm. *)
use import int.Int
(* Parameters.
Without loss of generality, we can take [x1=0] and [y1=0].
Thus the line to draw joins [(0,0)] to [(x2,y2)]
......@@ -9,11 +12,9 @@
[0 <= y2 <= x2]. The seven other cases can be easily
deduced by symmetry. *)
{
logic x2 : int
logic y2 : int
axiom First_octant : 0 <= y2 <= x2
}
(* The code.
[(best x y)] expresses that the point [(x,y)] is the best
......@@ -21,25 +22,23 @@ axiom First_octant : 0 <= y2 <= x2
The invariant relates [x], [y] and [e] and
gives lower and upper bound for [e] (see the Coq file). *)
{
use import int.Abs
logic best (x y:int) =
forall y':int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)
logic invariant (x y e:int) =
logic invariant_ (x y e:int) =
e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and
2 * (y2 - x2) <= e <= 2 * y2
lemma Invariant_is_ok : forall x y e:int. invariant x y e -> best x y
}
lemma Invariant_is_ok : forall x y e:int. invariant_ x y e -> best x y
let bresenham () =
let x = ref 0 in
let y = ref 0 in
let e = ref (2 * y2 - x2) in
while !x <= x2 do
invariant {0 <= !x and !x <= x2 + 1 and invariant !x !y !e }
invariant {0 <= !x and !x <= x2 + 1 and invariant_ !x !y !e }
variant { x2 + 1 - !x }
(* here we would plot (x, y) *)
assert { best !x !y };
......@@ -52,6 +51,7 @@ let bresenham () =
x := !x + 1
done
end
(*
Local Variables:
......
{
module M
(* preliminaries *)
......@@ -26,8 +25,6 @@
logic valid_array (a:first_free_addr) (n:int) (m:int) (r:array pointer) =
forall i:int. n <= i <= m -> valid a (A.get r i)
}
parameter alloc : ref first_free_addr
parameter new_pointer : tt:unit ->
......@@ -44,15 +41,11 @@ record Student =
end
*)
{
type student = (string, int)
logic invStudent (this:student) =
let (_,m) = this in 0 <= m <= 100
}
(*
record Course =
group Rstud: Student;
......@@ -69,8 +62,6 @@ record Course =
end
*)
{
type course = (region student, array pointer, int, int)
logic markSum (region student) int int (array pointer) : int
......@@ -119,8 +110,6 @@ end
and
sum = markSum rStud 0 (count-1) students
}
(*
fun CreateCourse(R:[Course]): [R]
consumes R^e
......@@ -187,10 +176,7 @@ fun SetMark(R:Course, c:[R], s: [c.Rstud], mark: int) : unit
*)
end
......
{
module M
use set.Fset as S
use array.Array as M
}
(* iteration on a set *)
......@@ -17,7 +17,6 @@ parameter set_next :
'a writes s
{ S.mem result (old !s) and !s = S.remove result (old !s) }
{
(* the graph *)
type vertex
......@@ -32,7 +31,7 @@ axiom G_succ_sound :
logic weight vertex vertex : int (* edge weight, if there is an edge *)
axiom Weight_nonneg : forall x y:vertex. weight x y >= 0
}
parameter eq_vertex :
x:vertex -> y:vertex -> {} bool { if result=True then x=y else x<>y }
......@@ -61,7 +60,7 @@ parameter q_is_empty :
parameter init :
src:vertex ->
{}
unit writes visited, q, d
unit writes visited q d
{ S.is_empty !visited and
!q = S.add src S.empty and
!d = M.set (old !d) src 0 }
......@@ -87,11 +86,9 @@ let relax u v =
(not S.mem v !visited and not S.mem v (old !q) and !q = S.add v (old !q) and
!d = M.set (old !d) v (M.get (old !d) u + weight u v)) }
{
logic min (m:vertex) (q:S.t vertex) (d:M.t vertex int) =
S.mem m q and
forall x:vertex. S.mem x q -> M.get d m <= M.get d x
}
parameter q_extract_min :
unit ->
......@@ -105,7 +102,6 @@ parameter q_extract_min :
shortest_path x y d =
there is a path from x to y of length d, and no shorter path *)
{
inductive path vertex vertex int =
| Path_nil :
forall x:vertex. path x x 0
......@@ -181,7 +177,6 @@ logic inv_succ2 (src:vertex) (s q : S.t vertex)
(forall x:vertex. S.mem x s ->
forall y:vertex. S.mem y (g_succ x) ->
(x<>u or (x=u and not S.mem y su)) -> S.mem y s or S.mem y q)
}
(* code *)
......@@ -210,6 +205,8 @@ let shortest_path_code (src:vertex) (dst:vertex) =
(forall v:vertex.
not S.mem v !visited -> forall dv:int. not path src v dv) }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/dijkstra"
......
module M
(* Fibonacci function with memoisation *)
{
(*
logic fib (n:int) : int =
if n <= 1 then 1 else fib (n-1) + fib (n-2)
......@@ -20,7 +20,6 @@
logic inv (t : table) =
forall x y : int. A.get t x = Some y -> y = fib x
}
parameter table : ref table
......@@ -45,12 +44,14 @@ let rec fibo n =
memo_fibo (n-1) + memo_fibo (n-2)
{ result = fib n and inv !table }
and memo_fibo n =
with memo_fibo n =
{ 0 <= n and inv !table }
try find n
with Not_found -> let fn = fibo n in add n fn; fn end
{ result = fib n and inv !table }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/fib"
......
module M
{
use import int.Gcd
use import int.ComputerDivision
}
let rec gcd u v variant { v } =
{ u >= 0 and v >= 0 }
......@@ -12,6 +11,8 @@ let rec gcd u v variant { v } =
gcd v (mod u v)
{ gcd u v result }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/gcd"
......
{
module M
use import int.ComputerDivision
use import int.Gcd
}
let gcd (x:int) (y:int) =
{ x >= 0 and y >= 0 }
......@@ -25,3 +25,4 @@ let gcd (x:int) (y:int) =
{ gcd x y result and
exists a b:int. a*x+b*y = result }
end
module M
{
use import list.Length
use import list.Sorted
use import list.Permut
}
let rec insert x l variant { length l } =
{ sorted l }
......@@ -21,6 +20,8 @@ let rec insertion_sort l variant { length l } =
end
{ sorted result and permut l result }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/insertion_sort_list.gui"
......
{
module M
logic sqr (x:int) : int = x * x
}
let isqrt (x:int) =
{ x >= 0 }
let count = ref 0 in
......@@ -20,4 +17,5 @@ let isqrt (x:int) =
!count
{ result >= 0 and sqr result <= x and x < sqr (result + 1) }
end
module M
(**** McCarthy's ``91'' function. *)
......@@ -12,7 +13,6 @@ let rec f91 (n:int) : int variant { 101-n } =
(* non-recursive version *)
{
logic f (x:int) : int =
if x >= 101 then x-10 else 91
......@@ -24,7 +24,6 @@ let rec f91 (n:int) : int variant { 101-n } =
clone import relations.Lex with type t1 = int, type t2 = int,
logic rel1 = lt_nat, logic rel2 = lt_nat
}
let f91_nonrec (n x : ref int) =
{ !n >= 1 }
......@@ -43,6 +42,7 @@ let f91_nonrec (n x : ref int) =
!x
{ result = iter_f (old !n) (old !x) }
end
(*
Local Variables:
......
module M
{
use import list.Length
use import list.Sorted
use import list.Append
......@@ -12,7 +12,6 @@
lemma Permut_cons_append:
forall x : 'a, l1 l2 : list 'a.
permut (append (Cons x l1) l2) (append l1 (Cons x l2))
}
let split l0 =
{ length l0 >= 2 }
......@@ -48,6 +47,8 @@ let rec mergesort l variant { length l } =
end
{ sorted result and permut l result }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/mergesort_list.gui"
......