updated bench/

parent 41691786
typing
------
- expression { e with f2 = e2 } is syntactic sugar for
{ f1 = e.f1; f2 = e2; f3 = e.f3 }
We would get better error messages if we would produce instead
{ f2 = e2; f1 = e.f1; f3 = e.f3 }
that is, with user-given fields first, then fields from e
See for instance bench/programs/bad-typing/with1.mlw
- the error message for
val foo (_x : int) : int
val f (x:int) : unit writes { foo.contents }
is "unbound symbol 'foo'", which is not correct
(is should rather be that "foo" has the wrong type)
- bench/programs/bad-to-keep/at1.mlw
should at least produce a warning (meaningless 'old')
docs
----
......
......@@ -165,12 +165,12 @@ invalid_goals bench/invalid
echo ""
echo "=== Checking theories ==="
goods theories
goods theories --type-only # FIXME remove --type-only
echo ""
echo "=== Checking modules ==="
goods modules
goods modules/mach
goods modules --type-only # FIXME remove --type-only
goods modules/mach --type-only # FIXME remove --type-only
echo ""
echo "=== Checking drivers ==="
......@@ -186,7 +186,7 @@ echo ""
echo "=== Checking good files ==="
goods bench/typing/good
goods bench/programs/good
goods bench/programs/good --type-only # FIXME remove --type-only
goods examples/bts
goods examples/tests
goods examples/tests-provers
......
......@@ -8,9 +8,3 @@ module M
= let (r,_) = a in r := !r + 1
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/bad-typing/at1"
End:
*)
module M
use import ref.Ref
(* reference would escape its scope *)
let test () =
let x = ref 0 in
fun y -> !x
end
......@@ -3,9 +3,3 @@ module M
use import int.Int
let foo () = for i = 1 to () do () done
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/bad-typing/for2"
End:
*)
module Horror
use import ref.Ref
let bad (ghost i : int) : ref int
ensures { !result = i }
= let r = ref 0 in
......
module M
use import int.Int
use import ref.Ref
let test1 (x: ref int)
requires { !x >= 0 }
ensures { !x >= old !x }
= while !x > 0 do
invariant { !x >= old !x }
x := !x - 1
done
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/bad-typing/old1"
End:
*)
module M
use import int.Int
use import ref.Ref
let test1 (x: ref int)
ensures { !x >= old !x }
requires { !x >= 0}
= x := !x - 1;
assert { !x >= old !x }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/bad-typing/old2"
End:
*)
(* old not allowed in programs *)
module Test
use import ref.Refint
let test (x: ref int) =
if !x = old !x then 1 else 2
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/bad-typing/old3"
End:
*)
\ No newline at end of file
module T1
predicate my_eq (x : ~'a) (y : 'a) = my_eq1 x y
with my_eq1 (x : 'a) (y : 'a) = my_eq2 x y
with my_eq2 (x : 'a) (y : 'a) = x = y
end
module T0
predicate eq (x y : ~'a)
end
module T1
predicate my_eq (x : 'a) (y : 'a) = my_eq1 x y
with my_eq1 (x : 'a) (y : 'a) = my_eq2 x y
with my_eq2 (x : 'a) (y : 'a) = x = y
clone T0 with predicate eq = my_eq
end
module T1
predicate my_eq (x : 'a) (y : 'a) = my_eq1 x y
with my_eq1 (x : 'a) (y : 'a) = my_eq2 x y
with my_eq2 (x : 'a) (y : 'a) = x = y
type t1 = { ghost f1 : int }
type t2 = Shell t1
let test1 (x: int) =
let r1 = Shell { f1 = x } in
my_eq r1 r1
end
module T1
predicate my_eq (x : 'a) (y : 'a) = my_eq1 x y
with my_eq1 (x : 'a) (y : 'a) = my_eq2 x y
with my_eq2 (x : 'a) (y : 'a) = x = y
let my_p_eq (x y : 'b) = my_eq x y
type t1 model { f1 : int }
type t2 = Shell t1
let test1 (x: t2) = my_p_eq x x
end
module T1
predicate my_eq (x : 'a) (y : 'a) = my_eq1 x y
with my_eq1 (x : 'a) (y : 'a) = my_eq2 x y
with my_eq2 (x : 'a) (y : 'a) = x = y
let my_p_eq (x y : ~'a) = my_eq x y
end
......@@ -2,7 +2,7 @@ module Bad
use import ref.Ref
function comp ~'a 'a : int
val function comp 'a 'a : int
let test () =
let rec f x y =
......
......@@ -2,7 +2,7 @@ module Bad
use import ref.Ref
function comp ~'a 'a : int
val function comp 'a 'a : int
let test () =
let r = ref 0 in
......
......@@ -2,7 +2,7 @@ module Bad
use import ref.Ref
function comp ~'a 'a : ()
val function comp 'a 'a : ()
let test z =
let rec f x =
......
module M
use import int.Int
use import ref.Ref
val x : ref int
let rec f5 (a b:ref int) variant { !a }
requires { !a >= 0 } ensures { result = old !a + old !b }
= if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end
(* partial application with non-generalizable effects is forbidden *)
let test_f5 () requires { !x >= 0 } ensures { result = old !x }
= let b = ref 0 in let f = f5 x in f b
end
module M
use import int.Int
use import ref.Ref
......@@ -44,7 +43,7 @@ let test_all_1 ()
(* from Cesar Munoz's CD3D *)
function d : int
val constant d : int
val vx : ref int
val vy : ref int
......@@ -55,11 +54,3 @@ let test_cd3d ()
ensures { result=1 -> !vx=0 /\ !vy=0 }
= if !vx=0 && !vy=0 && sq !vx + sq !vy < sq d then 1 else 2
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/booleans"
End:
*)
module M
exception Exception
......@@ -10,10 +9,3 @@ let f ()
raises { Exception -> true }
= f0 (f1 ())
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/complex_arg_1"
End:
*)
module M
exception Exception int
......@@ -10,10 +9,3 @@ val m (a:int) (b:int) : unit raises { Exception }
let test () raises { Exception } = (m ( assert { true } ; 0) 0)
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/complex_arg_2"
End:
*)
......@@ -20,9 +20,3 @@ let f (n : int) : int ensures { result <= 10 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/exceptions"
End:
*)
......@@ -39,6 +39,7 @@ let p6 () ensures { false } raises { E -> true | F _ -> false }
(* composition of exceptions with side-effect on a reference *)
use import int.Int
use import ref.Ref
val x : ref int
......@@ -104,9 +105,3 @@ let p17 () ensures { false } raises { E -> !x=0 }
= (x := 0; (raise E; x := 1))
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/exns"
End:
*)
......@@ -79,9 +79,3 @@ let test4d x
end
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/for"
End:
*)
......@@ -10,9 +10,3 @@ module Labels
= let (r,_) = a in r := !r + 1
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/labels"
End:
*)
......@@ -12,9 +12,3 @@ module M
end
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/list"
End:
*)
......@@ -32,8 +32,3 @@ let loop2 (u:unit) requires { !x <= 10 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/loops"
End:
*)
......@@ -6,20 +6,14 @@ module M
predicate even (x : int) = x = 2 * (div x 2)
predicate odd (x : int) = x = 2 * (div x 2) + 1
let rec is_even x : bool variant {x}
requires { 0 <= x }
ensures { result=True <-> even x }
= if x = 0 then True else is_odd (x-1)
let rec is_even x : bool variant {x}
requires { 0 <= x }
ensures { result = even x }
= if x = 0 then True else is_odd (x-1)
with is_odd x : bool variant {x}
requires { 0 <= x }
ensures { result=True <-> odd x }
= if x = 0 then False else is_even (x-1)
with is_odd x : bool variant {x}
requires { 0 <= x }
ensures { result = odd x }
= if x = 0 then False else is_even (x-1)
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/mutual"
End:
*)
......@@ -10,9 +10,3 @@ module T
with g (x: int) : int raises {MyExc} = f x
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/mutual_exns"
End:
*)
......@@ -10,7 +10,7 @@ module M
let g1 () ensures { q1 !r (old !r) (old !r) } = f1 !r
function foo int : int
val function foo int : int
predicate q int int int
val f (t:ref int) (x:int) : unit writes {t} ensures { q !t (old !t) x }
......@@ -18,9 +18,3 @@ module M
let g (t:ref int) ensures { q !t (old !t) (foo (old !t)) } = f t (foo !t)
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/oldify"
End:
*)
......@@ -67,9 +67,3 @@ val incrx2 () : int writes {x} ensures { !x = old !x + 1 /\ result = !x }
let p14 () requires { !x = 0 } ensures { result = 1 } = incrx2 ()
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/po"
End:
*)
......@@ -6,9 +6,3 @@ let p () ensures { result = 1 }
= if f True then f 1 else f 2
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/poly"
End:
*)
......@@ -31,10 +31,15 @@ module M
requires { !a >= 0 } ensures { !x = old !x + old !a }
= if !a > 0 then begin x := !x + 1; a := !a - 1; f4 a end
end
(** 5. The acid test:
partial application of a recursive function with effects *)
let rec f5 (a b:ref int) variant { !a }
requires { !a >= 0 } ensures { result = old !a + old !b }
= if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end
let test_f5 () requires { !x >= 0 } ensures { result = old !x }
= let b = ref 0 in let f = f5 x in f b
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/recfun"
End:
*)
......@@ -17,9 +17,3 @@ module LocalFunctions
let rec test2 () ensures { !r = 0 } = r := 0
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/scopes"
End:
*)
......@@ -22,9 +22,3 @@ let k ()
end
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/see"
End:
*)
......@@ -41,9 +41,3 @@ module M
done
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/set"
End:
*)
module T
let test () =
let a,b,c,d = (1,2,3,4) in ()
let _a,_b,_c,_d = (1,2,3,4) in ()
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/tuples"
End:
*)
......@@ -8,20 +8,11 @@ val x : ref int
val f () : unit writes {x} ensures { !x = 1 - old !x }
let p () =
'Init:
begin
let _t = () in ();
(f ());
(f ());
assert { !x = at !x 'Init };
()
end
label Init in
let _t = () in ();
(f ());
(f ());
assert { !x = !x at Init };
()
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/wpcalls"
End:
*)
theory Test
type t 'a
type t 'a
type u = t
end
theory Test
type t 'a
type t 'a
type u = t int int
end
......@@ -3,11 +3,11 @@
theory A
type t
axiom Ax : forall x:t. true
axiom Ax: forall x: t. x=x
end
theory B
use export A
axiom Ax : true
axiom Ax: forall x: t. x=x
end
theory A
type list 'a = Nil | Cons 'a (list 'a)
let f (l:list int) : int = match l with Cons x x -> 0 | Nil -> 1 end
end
theory T
type t = { mutable a:int }
end
theory T
type t = { a:int; b:int; }
type u = { c:int; d:int; }
goal g1 : let t = { a = 1; c = 2 } in true
type t = { a: int; b: int; }
type u = { c: int; d: int; }
goal g1 : let t = { a = 1; c = 2 } in true
end
theory Records
use import bool.Bool
type t = { a:int; b:bool; }
goal g1 : let t = { a = 1; b = 2 } in true
goal g1 : let t = { a = 1; b = 2 } in true
end
theory Records
type t = { a:int; b:int }
goal g1 :
goal g1 :
let t = { a = 1; b = 2 } in
let t = { t with a = () } in
true
......
theory Records
type t = { a:int; b:int }
type t = { a:int; b:int }
type t2 = { c:int; d:int }
goal g1 :
goal g1 :
let t = { a = 1; b = 2 } in
let t = { t with d = 3 } in
true
......
......@@ -285,8 +285,8 @@ theory NumOf
let rec function numof (p: int -> bool) (a b: int) : int
variant { b - a }
= if b <= a then 0 else
if p (b - 1) then 1 + numof p a (b - 1) else
numof p a (b - 1)
if p (b - 1) then 1 + numof p a (b - 1)
else numof p a (b - 1)
lemma Numof_bounds :
forall p : int -> bool, a b : int. a < b -> 0 <= numof p a b <= b - a
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment