Commit 250deb85 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Clean examples.

parent 1f4ad208
......@@ -253,7 +253,6 @@ goods bench/programs/bad-typing --parse-only
bads bench/typing/bad --type-only
bads bench/programs/bad-typing --type-only
goods bench/typing/x-bad --type-only
bads examples/bad-bts
echo ""
echo "=== Checking good files ==="
......
module M
predicate in_range (x : int) = -128 ≤ x ≤ 127
end
[tools fast]
prover = "alt-ergo"
prover = "cvc3"
prover = "z3"
prover = "simplify"
prover = "spass"
prover = "yices"
prover = "eprover"
timelimit = 1
[tools array]
command = "why3-cpulimit %t %m -s z3 -smt %f 2>&1"
driver = "/usr/local/share/why3/drivers/z3_array.drv"
#loadpath = "examples/programs"
#use = "meta.Partial_incomplete"
timelimit = 1
[tools instantiate]
prover = "cvc3"
prover = "z3"
prover = "spass"
prover = "yices"
prover = "eprover"
timelimit = 1
loadpath = "examples/programs"
use = "meta.Partial"
[probs funny]
file = "talk290.mlw"
file = "course.mlw"
file = "vstte10_aqueue.mlw"
file = "isqrt.mlw"
file = "insertion_sort_list.mlw"
file = "vacid_0_sparse_array.mlw"
file = "vacid_0_red_black_trees_harness.mlw"
file = "bresenham.mlw"
transform = "split_goal"
[bench fast_and_funny]
tools = fast
tools = array
tools = instantiate
probs = funny
timeline = "encodebench.time"
average = "encodebench.avg"
csv = "encodebench.csv"
theory Map
use list.List
function map (fn : 'a -> 'b) (l : list 'a) : list 'b = match l with
| Cons x r -> Cons (fn x) (map fn r)
| Nil -> Nil
end
predicate forall2 (pr : 'a -> 'b -> bool) (l1 : list 'a) (l2 : list 'b) =
match l1, l2 with
| Cons x1 r1, Cons x2 r2 -> pr x1 x2 /\ forall2 pr r1 r2
| _, _ -> true
end
use export int.Int
function double (l : list int) : list int = map (fun i -> i * 2) l
function double_let (l : list int) : list int =
let x = 2 in
map (fun i -> i * x) l
predicate lequal (l1 l2 : list int) =
forall2 (fun (i1 i2 : int) -> i1 = i2) l1 l2
end
theory Induction2
use list.List
use list.Length
predicate p (list 'a) (list 'b)
axiom Induction :
p (Nil : list 'a) (Nil : list 'b) ->
(forall x1:'a, x2:'b, l1:list 'a, l2:list 'b.
p l1 l2 -> p (Cons x1 l1) (Cons x2 l2)) ->
forall l1:list 'a, l2:list 'b. length l1 = length l2 -> p l1 l2
end
theory Test1
use export int.Int
use export list.List
use export list.Length
use Map as M
goal G1 : length (Cons 1 Nil) = 1
goal G2 : length (Cons 1 (Cons 2 Nil)) = 1 + 1
function zip (l1 : list 'a) (l2 : list 'b) : list ('a,'b) =
match l1, l2 with
| Cons x1 r1, Cons x2 r2 -> Cons (x1,x2) (zip r1 r2)
| _, _ -> Nil (* to make it total *)
end
predicate foo (l1 : list 'a) (l2 : list 'b) =
length (zip l1 l2) = length l1
clone Induction2 with predicate p = foo
lemma G3 : forall l1: list 'a, l2 : list 'b.
length l1 = length l2 ->
length (zip l1 l2) = length l1
goal G4 : zip (Cons 1 (Cons 2 Nil))
(Cons 1. (Cons 2. Nil)) =
Cons (1, 1.) (Cons (2, 2.) Nil)
goal G5 : forall l1: list 'a, l2 : list 'b, l3: list 'c, l4: list 'd.
length l1 = length l2 /\ length l2 = length l3 /\
length l3 = length l4 ->
length (zip (zip l1 l2) (zip l3 l4)) = length l3
end
[tools fast]
prover = "alt-ergo"
prover = "cvc3"
prover = "spass"
timelimit = 5
[probs funny]
file = "talk290.mlw"
transform = "split_goal"
[bench fast_and_funny]
tools = fast
probs = funny
timeline = "prgbench.time"
average = "prgbench.avg"
csv = "prgbench.csv"
theory Bidule
use set.SetMap
type a
type s = set a
function a : s
function b : s
function c : s
goal Union : forall s1 s2 : s. forall x : a.
mem x (union s1 s2) -> (mem x s1 \/ mem x s2)
goal Inter : forall s1 s2 : s. forall x : a.
mem x (inter s1 s2) -> (mem x s1 /\ mem x s2)
goal Union_inter : forall s1 s2 s3 : s.
equal (inter (union s1 s2) s3) (union (inter s1 s3) (inter s2 s3))
lemma Union_assoc : forall s1 s2 s3 : s.
equal (union (union s1 s2) s3) (union s1 (union s2 s3))
clone algebra.Assoc with type t = s, function op = union, goal Assoc
clone algebra.AC with type t = s, function op = union,
goal Assoc, goal Comm.Comm
end
2
5 5 5
5 5 5
5 5 5
15 5 5
15 5 5
15 5 5
5 15 5
5 15 5
5 15 5
5 15 5
5 5 15
5 5 15
5 5 15
5 5 15
theory Sorted
use int.Int
use real.Real
use map.Map
type array = map int real
type multi = map real int
function n : int = 4
predicate sorted (m : array) =
forall x y:int. x<=y -> Real.(<=) m[x] m[y]
function count(m : array) (i j : int) (v : real) : int
axiom Count :
forall m : array. forall i j : int. forall v : real. count m i j v =
(if i = j then 0 else
let c = count m (i+1) j v in
(if m[i] = v then c + 1 else c))
predicate model(m1 : array) (m2 : multi) =
forall v:real. count m1 1 (n+1) v = m2[v]
(*
function model_aux(m1 : array, i : int) : multi
axiom Model_aux_def1 :
forall m1 : array. forall i : int. forall v : real.
1 <= i /\ i <= n ->
get(model_aux(m1,i),v) =
if get(m1,i)=v then get(model_aux(m1,i+1),v) + 1
else get(model_aux(m1,i+1),v)
axiom Model_aux_def2 :
forall m1 : array. forall v : real. get(model_aux(m1,n+1),v) = 0
predicate model(m1 : array, m2 : multi) = model_aux(m1, 1) = m2
*)
(*axiom TPTP : 1 < 2 /\ 2 < 3 /\ 3 < 4 /\ 13 < 42 /\
0+1 = 1 /\ 1+1 = 2 /\ 2+1 = 3 /\ 3+1 = 4
axiom TPTP2 : forall x,y : real. x < y -> x<>y*)
goal G :
forall m1 : array.
m1[1] = 42. ->
m1[2] = 13. ->
m1[3] = 42. ->
m1[4] = 45. ->
forall m2 : array.
forall multi : multi.
model m1 multi ->
model m2 multi ->
sorted m2 ->
m2[1] = 13. /\
m2[2] = 42. /\
m2[3] = 42. /\
m2[4] = 45.
(* goal G_false :
forall m1 : array.
m1[1] = 42. ->
m1[2] = 13. ->
m1[3] = 42. ->
forall m2 : array.
forall multi : multi.
model m1 multi ->
model m2 multi ->
sorted m2 ->
m2[1] = 42. /\
m2[2] = 13. /\
m2[3] = 42.
*)
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="0" name="Alt-Ergo" version="2.2.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../nistonacci.mlw" proved="true">
<theory name="Top" proved="true">
<goal name="VC nist" expl="VC for nist" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC nistonacci" expl="VC for nistonacci" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="98"/></proof>
</goal>
<goal name="VC nist_ge_n" expl="VC for nist_ge_n" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="test" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
</file>
</why3session>
module TestFloat
use floating_point.Double
(*
function Sqrt (X : in Float) return Float
pre 1.0 <= X and X <= 2.0;
--# return R =>
--# R <= (1.0+4.0*PolyPaver.Floats.Eps_Rel)*PolyPaver.Exact.Sqrt(X);
is
R,S : Float;
begin
S := X;
R := PolyPaver.Floats.Add(PolyPaver.Floats.Multiply(0.5,X),0.5);
while R /= s loop
--# assert R in -0.25*X**2+X .. 0.25*X**2+1.0 ;
S := r;
R := PolyPaver.Floats.Multiply(0.5,
PolyPaver.Floats.Add(S,PolyPaver.Floats.Divide(X,S)));
end loop;
return R;
end Sqrt;
*)
end
\ No newline at end of file
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