Commit 1a8008ea authored by MARCHE Claude's avatar MARCHE Claude

a few more simple examples and tests

parent c4bcf6a2
theory T1
use import int.Int
goal G: 1 = 2
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="4">
<file name="../11244.why" expanded="true">
<theory name="T1" expanded="true">
<goal name="G" sum="ac87474f1a0a8f8f4c8c12cdf459a0f0" expanded="true">
<transf name="inline_goal" expanded="true">
<goal name="G.1" expl="1." sum="ac87474f1a0a8f8f4c8c12cdf459a0f0" expanded="true">
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
module M
use import int.Int
use import module ref.Ref
val x : ref int
goal A : !x = 0
goal B : (old !x) = 0
function f (n:int) : int = n + ! x
goal C : f(3) = 4
end
theory First
type t
constant c : t
predicate a
predicate p t
predicate q t
function f (t) : t
goal P1 : (forall x:t. p(x)) -> (exists x:t. p(x))
goal P5 : (forall x:t. p(x) -> p(f(x))) -> forall x:t.p(x) -> p(f(f(x)))
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="4">
<prover id="0" name="Alt-Ergo" version="0.94" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Yices" version="1.0.11" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.2" timelimit="5" memlimit="1000"/>
<prover id="4" name="Eprover" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="5" name="Spass" version="3.7" timelimit="5" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
<prover id="7" name="Simplify" version="1.5.4" timelimit="5" memlimit="1000"/>
<prover id="8" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="10" name="CVC4" version="1.3" timelimit="5" memlimit="1000"/>
<prover id="11" name="Vampire" version="0.6" timelimit="5" memlimit="1000"/>
<file name="../First.why" expanded="true">
<theory name="First" expanded="true">
<goal name="P1" sum="89e4abdc52745eaf94aeb280c8db8a10" expanded="true">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="unknown" time="0.01"/></proof>
<proof prover="10"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="P5" sum="4c2cebb4ede71be18820093b45c849a5" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01"/></proof>
<proof prover="5"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.01"/></proof>
<proof prover="10"><result status="valid" time="0.00"/></proof>
<proof prover="11"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
</why3session>
theory T1
use import int.Int
goal G: 1 = 2
end
\ No newline at end of file
module M
use import int.Int
use import module stdlib.Ref
(* preliminaries *)
use array.Array as A
type array 'a = A.t int 'a
logic injective (n:int) (m:int) (a:array 'a) =
forall i j:int. n <= i <= m -> n <= j <= m ->
A.get a i = A.get a j -> i = j
type string
(* Capucine memory model *)
type pointer
type region 'a = A.t pointer 'a
(*
type first_free_addr = int
logic valid (a:first_free_addr) (p:pointer) = p < a
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 ->
{ }
pointer
writes alloc
{ alloc = old alloc + 1 and result = old alloc }
*)
(*
record Student =
name: string;
mark: int
inv(this) { 0 <= this.mark <= 100 }
end
*)
type student = (string, int)
logic invStudent (this:student) =
let (_,m) = this in 0 <= m <= 100
(*
record Course =
group Rstud: Student;
students: array [Rstud]
count: int
sum: int
inv(this) {
count >= 0
and
injective(0, count-1, this.students)
and
this.sum = mark_sum(0,this.count-1,this.students)
}
end
*)
type course = (region student, array pointer, int, int)
(* markSum(r,i,j,a) donne \sigma_{k=i,j} get(r,a[k]).mark *)
logic markSum (region student) int int (array pointer) : int
(* axiom MarkSumEmpty :
forall region r:Student,
forall i j:int, forall a:(array pointer),
i > j -> markSum(r,i,j,a) = 0
*)
axiom MarkSumEmpty :
forall r:region student, i j:int, a : array pointer.
i > j -> markSum r i j a = 0
(* axiom MarkSumNonEmpty :
forall region r:Student,
forall i j:int, forall a:(array [r]),
i <= j ->
let p = array_get a j in
markSum(r,i,j,a) = markSum(r,i,j-1,a) + get(r,p).mark
*)
axiom MarkSumNonEmpty :
forall r:region student, i j:int, a : array pointer.
i <= j ->
let p = A.get a j in
let (_,mark) = A.get r p in
markSum r i j a = markSum r i (j-1) a + mark
(* a essayer mais pas essentiel
logic markSum (r:region student) (i:int) (j:int) (a:array pointer) : int =
if i > j then 0 else ...
*)
(*
lemma MarkSumFootprint:
forall n:int. forall s1: array(Student [R1]).
forall s2: array(Student [R2]).
(forall i:int. [0] <= [i] and [i] < [n] ==>
[!(select(s1,i) : Student[R1]).mark] =
[!(select(s2,i) : Student[R2]).mark])
==> [MarkSum(n, s1)] = [MarkSum(n,s2)]
*)
(*
lemma MarkSum_set_array_outside :
forall region r:Student. forall i j k:int, a: array [r], p:pointer.
not (i <= k <= j) ->
markSum(r,i,j,array_set(a,k,p)) = markSum(r,i,j,a)
*)
lemma MarkSum_set_array_outside :
forall r:region student, i j k:int, a: array pointer, p:pointer.
not (i <= k <= j) ->
markSum r i j (A.set a k p) = markSum r i j a
(*
lemma MarkSum_set_region_outside :
forall region r:Student. forall i j:int, a: array [r], p:pointer, s:student.
(forall k:int. i <= k <= j -> A.get a k <> p) ->
markSum (A.set r p s) i j a = markSum r i j a
*)
lemma MarkSum_set_region_outside :
forall r:region student, i j:int, a: array pointer, p:pointer, s:student.
(forall k:int. i <= k <= j -> A.get a k <> p) ->
markSum (A.set r p s) i j a = markSum r i j a
logic invCourse (alloc:first_free_addr) (this:course) =
let (rStud,students,count,sum) = this in
count >= 0
and
valid_array alloc 0 (count - 1) students
and
injective 0 (count - 1) students
and
sum = markSum rStud 0 (count-1) students
(*
fun CreateCourse(R:[Course]): [R]
consumes R^e
produces R^c
=
let c = new Course [R] in
c.count = 0;
c.sum = 0;
pack c;
c
*)
let createCourse (r: (ref (region course))) : pointer =
{ }
let c = new_pointer () in
let (rStud,student,count,sum) = A.get !r c in
let newc = (rStud,student,0,0) in
r := A.set !r c newc;
assert { invCourse alloc newc };
c
{ valid alloc result }
(*
fun RegisterStudent(R:[Course], c: [R], name: string): [R.Rstud]
consumes R^c
produces R^c
=
region S in
let s = new Student[S] in
s := (name, 0);
assert forall i:int, array_get c.students i in rStud;
(adoptregion S as R.R_s);
" assume forall p:pointer. p in old(R.R_S) -> p <> s "
assert [MarkSum(!(!c.students))] = [old(MarkSum(!(!c.students)))];
(focus !c.students) := add(!(!c.students), s);
c := (!c.students, !c.count + 1, !c.total, !c.4);
s
*)
let registerStudent
(r: (ref (region course))) (c:pointer) (name:string) : pointer =
{ valid alloc c and invCourse alloc (A.get r c) }
let s = new_pointer () in
let (rStud,student,count,sum) = A.get !r c in
let newstud = (name,0) in
assume { forall p:pointer. in_region(p,old rStud) -> p <> s } ;
let newc = (A.set rStud s newstud,A.set student count s,count+1,sum) in
r := A.set !r c newc;
assert { invCourse alloc newc };
s
{ valid alloc result }
(*
fun SetMark(R:Course, c:[R], s: [c.Rstud], mark: int) : unit
consumes R^c
produces R^c
{
unpack c (* c.Rstud^G, R^o *)
let region Rs:Student
let s' = focus s as Rs (* Rs -o c.Rstud, Rs^c, R^o *)
unpack s' (* Rs -o c.Rstud, Rs^o, R^o *)
s'.mark <- mark;
pack s';
pack c
}
*)
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/course"
End:
*)
theory T
goal G "expl:Coucou" "file:toto.c" "line:3" "begin:7" "end:14" :
1=2
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