Commit 3feba002 authored by MARCHE Claude's avatar MARCHE Claude

prover example: update sessions in progress

parent 53bed3cb
......@@ -68,7 +68,7 @@ module Logic
function pop (l:list 'a) : list 'a = match l with
| Nil -> default
| Cons x q -> q
| Cons _x q -> q
end
function unroll (tm:int) (t0:int) (h:list int) (b:func int (list 'a))
......
......@@ -70,7 +70,8 @@ endif
replay:
for i in $(MLWUTIL) $(MLWIMPL); do \
why3 replay -q -L . $$i ; \
echo "Replaying $$i..." ; \
why3 $(WHY3FLAGS) replay -q $$i ; \
done
depend: .depend
......
module Funcs
use import option.Option
use import Functions.Func
(* Abstraction definition axiom :
constant some : func 'a (option 'a) = (\ x:'a. Some x) *)
constant some : func 'a (option 'a)
axiom some_def : forall x:'a. some x = Some x
(* Abstraction definition axiom :
constant ocase (f:func 'a 'b) (d:'b) : func (option 'a) 'b =
(\ x:'a. match x with None -> d | Some x -> f x end) *)
function ocase (f:func 'a 'b) (d:'b) : func (option 'a) 'b
axiom ocase_def : forall f:func 'a 'b,d:'b,x:option 'a.
ocase f d x = match x with None -> d | Some x -> f x end
lemma ocase_some : forall f:func 'a 'b,d:'b,x:'a.
ocase f d (Some x) = f x
lemma ocase_none : forall f:func 'a 'b,d:'b.
......@@ -24,14 +24,14 @@ module Funcs
ensures { rcompose some (ocase f d) = f }
=
assert { extensionalEqual (rcompose some (ocase f d)) f }
function omap (f:func 'a 'b) (x:option 'a) : option 'b = match x with
| None -> None
| Some x -> Some (f x)
end
function olift (f:func 'a 'b) : func (option 'a) (option 'b) = ocase (compose some f) None
lemma olift_def : forall f:func 'a 'b,x:option 'a. olift f x = omap f x
lemma olift_none : forall f:func 'a 'b. olift f None = None
lemma olift_some : forall f:func 'a 'b,x:'a. olift f (Some x) = Some (f x)
lemma olift_none_inversion : forall f:func 'a 'b,x:option 'a. olift f x = None <-> x = None
......@@ -41,26 +41,25 @@ module Funcs
=
match x with
| None -> ()
| Some x' -> ()
| Some _x' -> ()
end
let lemma olift_identity (u:unit) : unit
ensures { olift (identity:func 'a 'a) = identity }
=
assert { extensionalEqual (olift (identity:func 'a 'a)) identity }
let lemma olift_composition (g:func 'b 'c) (f:func 'a 'b) : unit
ensures { compose (olift g) (olift f) = olift (compose g f) }
=
assert { extensionalEqual (compose (olift g) (olift f)) (olift (compose g f)) }
lemma olift_some_commutation : forall f:func 'a 'b.
compose some f = compose (olift f) some
let lemma olift_update (f:func 'a 'b) (x:'a) (y:'b) : unit
ensures { olift (f[x<-y]) = (olift f)[Some x <- Some y] }
=
assert { extensionalEqual (olift (f[x <- y])) ((olift f)[Some x <- Some y]) }
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!
Please register or to comment