Commit c3718467 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

finished implem of new construct abstract + test + doc

parent c9a37594
......@@ -80,6 +80,9 @@
function x : 'a
(cf: en caml cela ne marche pas)
* new language constructs
** sandbox, abstract
* efficiency issues
- understand problems when large number of goals (cf D Mentré examples)
- also: BTS 13736
......
......@@ -285,7 +285,7 @@ The corresponding rules for computing WP are as follows:
WP(\texttt{abstract}~e~\{ Q \mid exn_i \Rightarrow R_i \} ,
Q' \mid exn_i \Rightarrow R'_i) = \\
\qquad\qquad WP(e,Q \mid exn_i \Rightarrow R_i) \land
\forall result, \epsilon, Q \rightarrow Q' \land R_i \Rightarrow R'_i
\forall result, \epsilon, Q \rightarrow Q' \land R_i \rightarrow R'_i
\end{array}
\]
......
......@@ -640,9 +640,9 @@ and wp_desc env rm e q = match e.expr_desc with
let p = wp_label e (wp_expl "precondition" c.c_pre) in
let p = t_label ~loc:e.expr_loc p.t_label p in
wp_and p w
| Eabstract(e1,((_normal,_exns) as post)) ->
| Eabstract(e1,post) ->
let w1 = wp_expr env rm e1 post in
let w2 = t_false (* TODO *) in
let w2 = opaque_wp env rm e1.expr_effect.E.writes post q in
wp_and ~sym:true w1 w2
and wp_triple env rm bl (p, e, q) =
......
......@@ -111,6 +111,22 @@ module M
end
module CodeAnnotations
use import int.Int
use import module ref.Ref
let f (x:int) : int =
{ }
let y = ref 0 in
abstract y := !y + 1 { !y > 0 };
!y
{ result = 1 (* should not be proved !*) }
end
(*
Local Variables:
compile-command: "unset LANG; make -C .. testl-ide"
......
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