try to add some ensures to abstract when none is given

when a abstract construct has no user postcondition
we try to add one by purifying the program expression,
that is, ensures { result = t }, where t is a term
obtained from the program expression e

program expression e may involve function calls with
preconditions (e.g. array access, division)

the purpose of this change is to limit the number
of VCs by surrounding some program expressions with
abstract (e.g. if abstract i >= 0 && a[i] = 0 end then ...)

this is not a conservative change: one may have to
add ensures { true } to recover the previous behavior
(yet there is no example in the gallery of abstract e
with e pure and no post)

note: we might want to do that automatically for if-then-else
expressions (including lazy operators)
parent 956f2ac6
......@@ -1337,7 +1337,17 @@ and try_expr keep_loc uloc env ({de_dvty = argl,res} as de0) =
check_user_effect e spec [] dsp;
let speci = spec_invariant env e.e_syms.syms_pv e.e_vty spec in
(* we do not require invariants on free variables *)
e_abstract e { speci with c_pre = spec.c_pre }
let spec = { speci with c_pre = spec.c_pre } in
(* no user post => we try to purify *)
let spec = if dsp.ds_post <> [] then spec else match e_purify e with
| Some t ->
let vs, f = Mlw_ty.open_post spec.c_post in
let f = t_and_simp (t_equ_simp (t_var vs) t) f in
let f = t_label_add Split_goal.stop_split f in
let post = Mlw_ty.create_post vs f in
{ spec with c_post = post }
| None -> spec in
e_abstract e spec
| DEmark (id,de) ->
let ld = create_let_defn id Mlw_wp.e_now in
let env = add_let_sym env ld.let_sym in
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