Commit b4380d74 authored by Andrei Paskevich's avatar Andrei Paskevich

WhyML: defensive "any"

parent f47f00e8
......@@ -83,6 +83,9 @@ module BFS
function (!!) (s: B.t) : set vertex = B.contents s
val pick_succ (v: vertex) : B.t
ensures { !!result = succ v }
(* function fill_next fills set next with the unvisited successors of v *)
let fill_next (s t v: vertex) (visited current next: B.t) (d:ref int)
requires { inv s t !!visited !!current !!next !d /\
......@@ -91,7 +94,7 @@ module BFS
ensures { inv s t !!visited !!current !!next !d /\
subset (succ v) !!visited /\
(forall x: vertex. closure !!visited !!current !!next x) }
= let acc = any B.t ensures { !!result = succ v } in
= let acc = pick_succ v in
while not (B.is_empty acc) do
invariant {
inv s t !!visited !!current !!next !d /\
......
......@@ -106,6 +106,28 @@
| Pwild -> sp
| _ -> { sp with sp_post = List.map apply sp.sp_post }
let we_attr = Ident.create_attribute "expl:witness existence"
let pre_of_any any_loc ty ql =
if ql = [] then [] else
let ri loc = { id_str = "result"; id_loc = loc; id_ats = [] } in
let rt loc = { term_desc = Tident (Qident (ri loc)); term_loc = loc } in
let rec case (loc, pfl) = match pfl with
| [{ pat_desc = Ptree.Pparen p; pat_loc = loc}, f] -> case (loc, [p,f])
| [{ pat_desc = Ptree.Pwild | Ptree.Ptuple [] }, f] -> f
| [{ pat_desc = Ptree.Pvar { id_str = "result" } }, f] -> f
| [{ pat_desc = Ptree.Pvar id }, f] ->
{ term_desc = Tlet (id, rt loc, f); term_loc = loc }
| _ -> { term_desc = Tcase (rt loc, pfl); term_loc = loc } in
let mk_t desc = { term_desc = desc; term_loc = any_loc } in
let rec join ql = match ql with
| [] -> assert false (* never *)
| [q] -> case q
| q::ql -> mk_t (Tbinop (case q, Dterm.DTand_asym, join ql)) in
let bl = [any_loc, Some (ri any_loc), false, Some ty] in
let p = mk_t (Tquant (Dterm.DTexists, bl, [], join ql)) in
[mk_t (Tattr (ATstr we_attr, p))]
let error_param loc =
Loc.errorm ~loc "cannot determine the type of the parameter"
......@@ -850,7 +872,19 @@ single_expr_:
Efun ($2, None, Ity.MaskVisible, spec_union $3 $5, e) }
| ANY return_named spec
{ let pat, ty, mask = $2 in
Eany ([], Expr.RKnone, Some ty, mask, apply_return pat $3) }
let loc = floc $startpos $endpos in
let spec = apply_return pat $3 in
if spec.sp_writes <> [] then Loc.errorm ~loc
"this expression should not produce side effects";
if spec.sp_xpost <> [] then Loc.errorm ~loc
"this expression should not raise exceptions";
if spec.sp_alias <> [] then Loc.errorm ~loc
"this expression cannot have alias restrictions";
if spec.sp_diverge then Loc.errorm ~loc
"this expression must terminate";
let pre = pre_of_any loc ty spec.sp_post in
let spec = { spec with sp_pre = spec.sp_pre @ pre } in
Eany ([], Expr.RKnone, Some ty, mask, spec) }
| VAL ghost kind attrs(lident_rich) mk_expr(val_defn) IN seq_expr
{ Elet ($4, $2, $3, $5, $7) }
| MATCH seq_expr WITH ext_match_cases END
......
......@@ -86,9 +86,8 @@ module Set
= fun x -> not s[x]
(** arbitrary element *)
let ghost function choose(s: set 'a): 'a
val ghost function choose(s: set 'a): 'a
ensures { not (is_empty s) -> mem result s }
= any 'a ensures { not (is_empty s) -> mem result s }
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