Commit df2a638a by Francois Bobot

### transformation à la nouvelle syntax de why de test-bobot.why

parent 3b7eda36
 ... @@ -94,7 +94,7 @@ ... @@ -94,7 +94,7 @@ :group 'why :type 'string) :group 'why :type 'string) (defun why-command-line (file) (defun why-command-line (file) (concat why-prog-name " -" why-prover " " why-options " " file)) (concat why-prog-name " -P " why-prover " " why-options " " file)) (defun why-find-alternate-file () (defun why-find-alternate-file () "switch to the proof obligations buffer" "switch to the proof obligations buffer" ... ...
 ... @@ -4,8 +4,8 @@ ... @@ -4,8 +4,8 @@ theory Test_inline_trivial theory Test_inline_trivial type t type t logic c : t logic c : t logic eq(x:'a, y:'a) = x=y logic eq (x y :'a) = x=y goal G : eq(c,c) goal G : eq c c end end theory Test_ind theory Test_ind ... @@ -31,8 +31,8 @@ end ... @@ -31,8 +31,8 @@ end theory Test_simplify_array theory Test_simplify_array use import array.Array use import array.Array goal G : forall x,y:int. forall m: (int,int) t. goal G : forall x y:int. forall m: t int int. select(store(m,y,x),y) = x select (store m y x) y = x end end theory Test_conjunction theory Test_conjunction ... @@ -49,7 +49,7 @@ theory Split_conj ... @@ -49,7 +49,7 @@ theory Split_conj (*goal G : forall x,y,z:int. ((p(x) -> p(y)) and ((not p(x)) -> p(z))) -> ((p(x) and p(y)) or ((not p(x)) and p(z)))*) (*goal G : forall x,y,z:int. ((p(x) -> p(y)) and ((not p(x)) -> p(z))) -> ((p(x) and p(y)) or ((not p(x)) and p(z)))*) (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) and p(y)) or ((not p(x)) and p(z)))*) (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) and p(y)) or ((not p(x)) and p(z)))*) (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) -> (if p(x) then p(y) else p(z))*) (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) -> (if p(x) then p(y) else p(z))*) goal G : forall x,y,z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z)) goal G : forall x y z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z)) (*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) and (not p(x)) or ((p(z)) and (p(x))))) *) (*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) and (not p(x)) or ((p(z)) and (p(x))))) *) (*goal G : forall x,y,z:int. (p(x) or p(y)) -> p(z)*) (*goal G : forall x,y,z:int. (p(x) or p(y)) -> p(z)*) end end ... @@ -59,20 +59,20 @@ end ... @@ -59,20 +59,20 @@ end theory TestEnco theory TestEnco use import int.Int use import int.Int type 'a mytype type mytype 'a logic id(x: int) : int = x logic id(x: int) : int = x logic id2(x: int) : int = id(x) logic id2(x: int) : int = id(x) logic succ(x:int) : int = id(x+1) logic succ(x:int) : int = id(x+1) goal G : (forall x:int. x=x) or goal G : (forall x:int. x=x) or (forall x:int. x=x+1) (forall x:int. x=x+1) logic p('a ) : 'a mytype logic p('a ) : mytype 'a logic p2('a mytype) : 'a logic p2(mytype 'a) : 'a type toto type toto logic f (toto) : toto mytype logic f (toto) : mytype toto logic g (int mytype) : toto logic g (mytype int) : toto logic h (int) : toto mytype logic h (int) : mytype toto axiom A1 : forall x : 'a mytype. p(p2(x)) = x axiom A1 : forall x : mytype 'a. p(p2(x)) = x goal G2 : forall x:int. f(g(p(x))) = h(x) goal G2 : forall x:int. f(g(p(x))) = h(x) end end ... @@ -94,7 +94,7 @@ end ... @@ -94,7 +94,7 @@ end theory TestBuiltin_bool theory TestBuiltin_bool use import bool.Bool use import bool.Bool goal G : xorb(True,False) = True goal G : xorb True False = True end end ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!