Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit aef6cb4c authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

programs: my first WP

parent 995f52a6
...@@ -114,6 +114,7 @@ and recfun _env _def = ...@@ -114,6 +114,7 @@ and recfun _env _def =
module State : sig module State : sig
type t type t
val create : E.t -> t val create : E.t -> t
val fresh_label: env -> label
val push_label : env -> label -> t -> t val push_label : env -> label -> t -> t
val havoc : env -> ?pre:label -> E.t -> t -> t val havoc : env -> ?pre:label -> E.t -> t -> t
val term : env -> t -> term -> term val term : env -> t -> term -> term
...@@ -186,13 +187,34 @@ end = struct ...@@ -186,13 +187,34 @@ end = struct
end end
let rec wprec env s e = match e.expr_desc with let wp_binder (x, tv) f = match tv with
| Tpure _ -> f_forall [x] [] f
| Tarrow _ -> f
let wp_binders = List.fold_right wp_binder
let rec wp_expr env s e q = match e.expr_desc with
| Elogic t -> | Elogic t ->
assert false (*TODO*) let t = State.term env s t in
begin match q with
| Some ((v,q),_) -> f_let v t q
| None -> f_true
end
| Efun (bl, t) ->
let f = wp_triple env s t in
wp_binders bl f
| _ -> | _ ->
f_true (* TODO *) f_true (* TODO *)
let wp env _ls e = wprec env (State.create e.expr_effect) e and wp_triple env s (p,e,q) =
let s = State.create e.expr_effect in
let old = State.fresh_label env in
let s = State.push_label env old s in
(* FIXME: replace old(t) by at(t,old) in q *)
let f = wp_expr env s e (Some q) in
f_implies (State.fmla env s p) f
let wp env e = wp_expr env (State.create e.expr_effect) e None
let wp_recfun _env _l _def = f_true (* TODO *) let wp_recfun _env _l _def = f_true (* TODO *)
...@@ -207,7 +229,7 @@ let decl env = function ...@@ -207,7 +229,7 @@ let decl env = function
(* DEBUG *) (* DEBUG *)
printf "@[--effect %a-----@\n %a@]@\n---------@." printf "@[--effect %a-----@\n %a@]@\n---------@."
Pretty.print_ls ls print_type_v e.expr_type_v; Pretty.print_ls ls print_type_v e.expr_type_v;
let f = wp env ls e in let f = wp env e in
let env = add_wp_decl ls f env in let env = add_wp_decl ls f env in
let env = add_global ls e.expr_type_v env in let env = add_global ls e.expr_type_v env in
env env
...@@ -228,3 +250,9 @@ let decl env = function ...@@ -228,3 +250,9 @@ let decl env = function
let file uc dl = let file uc dl =
let env = List.fold_left decl (empty_env uc) dl in let env = List.fold_left decl (empty_env uc) dl in
Theory.close_theory env.uc Theory.close_theory env.uc
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
...@@ -13,8 +13,8 @@ parameter imp_sub : ...@@ -13,8 +13,8 @@ parameter imp_sub :
parameter r : int ref parameter r : int ref
let ff () = let ff () =
{ !r = 1 } { true }
!r + 2 1+2
{ result = 3 } { result = 3 }
......
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