programs: the 'downto' variant of the for loop

parent b45cda99
(* for loop with invariant *)
let test () =
let test1 () =
let x = ref 0 in
for i = 1 to 10 do
invariant { !x = i-1 }
......@@ -41,6 +41,42 @@ let test4 x =
end
{ result=True <-> 0 <= x <= 10 }
(* and now downto *)
let test1d () =
let x = ref 11 in
for i = 10 downto 1 do
invariant { !x = i+1 }
x := !x - 1
done;
assert { !x = 1 }
let test2d () =
let x = ref 0 in
for i = 1 downto 2 do
x := 1
done;
assert { !x = 0 }
let test3d () =
{ }
for i = 10 downto 1 do invariant { i < 10 -> false }
raise E
done
{ false } | E -> { true }
let test4d x =
{ }
try
for i = 10 downto 0 do
invariant { x > 10 or x <= i }
if i = x then raise E
done;
False
with E ->
True
end
{ result=True <-> 0 <= x <= 10 }
(*
Local Variables:
......
......@@ -29,7 +29,7 @@
'("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
'("{\\([^}]*\\)}" . font-lock-type-face)
`(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type")) . font-lock-builtin-face)
`(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "do" "done" "label" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses")) . font-lock-keyword-face)
`(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses")) . font-lock-keyword-face)
; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
)
"Minimal highlighting for Why mode")
......
......@@ -56,8 +56,10 @@ type env = {
ls_orb : lsymbol;
ls_notb : lsymbol;
ls_unit : lsymbol;
ls_lt : lsymbol;
ls_gt : lsymbol;
ls_le : lsymbol;
ls_ge : lsymbol;
ls_add : lsymbol;
}
......@@ -152,8 +154,10 @@ let empty_env uc = {
ls_orb = find_ls uc ["orb"];
ls_notb = find_ls uc ["notb"];
ls_unit = find_ls uc ["Tuple0"];
ls_lt = find_ls uc ["infix <"];
ls_gt = find_ls uc ["infix >"];
ls_le = find_ls uc ["infix <="];
ls_ge = find_ls uc ["infix >="];
ls_add = find_ls uc ["infix +"];
}
......
......@@ -56,8 +56,10 @@ type env = private {
ls_orb : lsymbol;
ls_notb : lsymbol;
ls_unit : lsymbol;
ls_lt : lsymbol;
ls_gt : lsymbol;
ls_le : lsymbol;
ls_ge : lsymbol;
ls_add : lsymbol;
}
......
......@@ -48,6 +48,7 @@
"check", CHECK;
"do", DO;
"done", DONE;
"downto", DOWNTO;
"else", ELSE;
"end", END;
"exception", EXCEPTION;
......
......@@ -116,7 +116,7 @@
/* keywords */
%token ABSURD AND ANY AS ASSERT ASSUME BEGIN CHECK DO DONE ELSE END
%token ABSURD AND ANY AS ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO ELSE END
%token EXCEPTION FOR
%token FUN GHOST IF IN INVARIANT LABEL LET MATCH NOT OF PARAMETER
%token RAISE RAISES READS REC
......@@ -317,8 +317,8 @@ expr:
mk_expr (Eif ($2, $5,
mk_expr (Eraise (exit_exn (), None)))))),
[exit_exn (), None, mk_expr Eskip])) }
| FOR lident EQUAL expr TO expr DO loop_invariant expr DONE
{ mk_expr (Efor ($2, $4, $6, $8, $9)) }
| FOR lident EQUAL expr for_direction expr DO loop_invariant expr DONE
{ mk_expr (Efor ($2, $4, $5, $6, $8, $9)) }
| ABSURD
{ mk_expr Eabsurd }
| expr COLON pure_type
......@@ -434,6 +434,11 @@ assertion_kind:
| CHECK { Acheck }
;
for_direction:
| TO { To }
| DOWNTO { Downto }
;
loop_annotation:
| loop_invariant opt_variant { { loop_invariant = $1; loop_variant = $2 } }
;
......
......@@ -42,6 +42,8 @@ type loop_annotation = {
loop_variant : variant option;
}
type for_direction = To | Downto
type effect = {
pe_reads : ident list;
pe_writes : ident list;
......@@ -88,7 +90,7 @@ and expr_desc =
| Eabsurd
| Eraise of ident * expr option
| Etry of expr * (ident * ident option * expr) list
| Efor of ident * expr * expr * lexpr option * expr
| Efor of ident * expr * for_direction * expr * lexpr option * expr
(* annotations *)
| Eassert of assertion_kind * lexpr
| Elabel of ident * expr
......
......@@ -29,6 +29,8 @@ type assertion_kind = Pgm_ptree.assertion_kind
type lazy_op = Pgm_ptree.lazy_op
type for_direction = Pgm_ptree.for_direction
(*****************************************************************************)
(* phase 1: introduction of destructive types *)
......@@ -90,7 +92,7 @@ and dexpr_desc =
| DEabsurd
| DEraise of Term.lsymbol * dexpr option
| DEtry of dexpr * (Term.lsymbol * string option * dexpr) list
| DEfor of ident * dexpr * dexpr * Denv.dfmla option * dexpr
| DEfor of ident * dexpr * for_direction * dexpr * Denv.dfmla option * dexpr
| DEassert of assertion_kind * Denv.dfmla
| DElabel of string * dexpr
......@@ -149,8 +151,8 @@ and iexpr_desc =
| IEabsurd
| IEraise of Term.lsymbol * iexpr option
| IEtry of iexpr * (Term.lsymbol * Term.vsymbol option * iexpr) list
| IEfor of
Term.vsymbol * Term.vsymbol * Term.vsymbol * Term.fmla option * iexpr
| IEfor of Term.vsymbol * Term.vsymbol * for_direction * Term.vsymbol *
Term.fmla option * iexpr
| IEassert of assertion_kind * Term.fmla
| IElabel of label * iexpr
......@@ -186,8 +188,8 @@ and expr_desc =
| Eabsurd
| Eraise of Term.lsymbol * expr option
| Etry of expr * (Term.lsymbol * Term.vsymbol option * expr) list
| Efor of
Term.vsymbol * Term.vsymbol * Term.vsymbol * Term.fmla option * expr
| Efor of Term.vsymbol * Term.vsymbol * for_direction * Term.vsymbol *
Term.fmla option * expr
| Eassert of assertion_kind * Term.fmla
| Elabel of label * expr
......
......@@ -427,7 +427,7 @@ and dexpr_desc env loc = function
(ls, x, h)
in
DEtry (e1, List.map handler hl), e1.dexpr_type
| Pgm_ptree.Efor (x, e1, e2, inv, e3) ->
| Pgm_ptree.Efor (x, e1, d, e2, inv, e3) ->
let e1 = dexpr env e1 in
expected_type e1 (dty_int env.env);
let e2 = dexpr env e2 in
......@@ -436,7 +436,7 @@ and dexpr_desc env loc = function
let inv = option_map (dfmla env.denv) inv in
let e3 = dexpr env e3 in
expected_type e3 (dty_unit env.env);
DEfor (x, e1, e2, inv, e3), dty_unit env.env
DEfor (x, e1, d, e2, inv, e3), dty_unit env.env
| Pgm_ptree.Eassert (k, le) ->
DEassert (k, dfmla env.denv le), dty_unit env.env
......@@ -712,7 +712,7 @@ and iexpr_desc gl env loc ty = function
(ls, x, iexpr gl env h)
in
IEtry (iexpr gl env e, List.map handler hl)
| DEfor (x, e1, e2, inv, e3) ->
| DEfor (x, e1, d, e2, inv, e3) ->
let e1 = iexpr gl env e1 in
let e2 = iexpr gl env e2 in
let vx = create_vsymbol (id_user x.id x.id_loc) e1.iexpr_type in
......@@ -723,7 +723,7 @@ and iexpr_desc gl env loc ty = function
let v2 = create_vsymbol (id_user "for_end" loc) e2.iexpr_type in
IElet (v1, e1, mk_iexpr loc ty (
IElet (v2, e2, mk_iexpr loc ty (
IEfor (vx, v1, v2, inv, e3)))))
IEfor (vx, v1, d, v2, inv, e3)))))
| DEassert (k, f) ->
let f = Denv.fmla env f in
......@@ -1065,14 +1065,14 @@ and expr_desc gl env loc ty = function
List.fold_left (fun e (_,_,h) -> E.union e h.expr_effect) ef hl
in
Etry (e1, hl), tpure ty, ef
| IEfor (x, v1, v2, inv, e3) ->
| IEfor (x, v1, d, v2, inv, e3) ->
let env = add_local x (tpure v1.vs_ty) env in
let e3 = expr gl env e3 in
let ef = match inv with
| Some f -> fmla_effect gl e3.expr_effect f
| None -> e3.expr_effect
in
Efor (x, v1, v2, inv, e3), type_v_unit gl, ef
Efor (x, v1, d, v2, inv, e3), type_v_unit gl, ef
| IEassert (k, f) ->
let ef = fmla_effect gl E.empty f in
......@@ -1179,8 +1179,8 @@ let rec fresh_expr gl ~term locals e = match e.expr_desc with
| Etry (e1, hl) ->
fresh_expr gl ~term:false locals e1;
List.iter (fun (_, _, e2) -> fresh_expr gl ~term locals e2) hl
| Efor (_, _, _, _, e3) ->
fresh_expr gl ~term:false locals e3
| Efor (_, _, _, _, _, e1) ->
fresh_expr gl ~term:false locals e1
| Elabel (_, e) ->
fresh_expr gl ~term locals e
......
......@@ -354,7 +354,7 @@ and wp_desc env e q = match e.expr_desc with
let q1 = saturate_post e1.expr_effect (fst q) q in
let q1 = filter_post e1.expr_effect (make_post q1) in
wp_expr env e1 q1
| Efor (x, v1, v2, inv, e1) ->
| Efor (x, v1, d, v2, inv, e1) ->
(* wp(for x = v1 to v2 do inv { I(x) } e1, Q, R) =
v1 > v2 -> Q
and v1 <= v2 -> I(v1)
......@@ -362,11 +362,15 @@ and wp_desc env e q = match e.expr_desc with
I(i) -> wp(e1, I(i+1), R)
and I(v2+1) -> Q *)
let (res, q1), _ = q in
let v1_gt_v2 = f_app env.ls_gt [t_var v1; t_var v2] in
let v1_le_v2 = f_app env.ls_le [t_var v1; t_var v2] in
let gt, le, incr = match d with
| Pgm_ptree.To -> env.ls_gt, env.ls_le, t_int_const "1"
| Pgm_ptree.Downto -> env.ls_lt, env.ls_ge, t_int_const "-1"
in
let v1_gt_v2 = f_app gt [t_var v1; t_var v2] in
let v1_le_v2 = f_app le [t_var v1; t_var v2] in
let inv = match inv with Some inv -> inv | None -> f_true in
let wp1 =
let xp1 = t_app env.ls_add [t_var x; t_int_const "1"] ty_int in
let xp1 = t_app env.ls_add [t_var x; incr] ty_int in
let post = f_subst (subst1 x xp1) inv in
let q1 = saturate_post e1.expr_effect (res, post) q in
wp_expr env e1 q1
......@@ -376,10 +380,10 @@ and wp_desc env e q = match e.expr_desc with
(quantify env e.expr_effect
(wp_and ~sym:true
(wp_forall env x
(wp_implies (wp_and (f_app env.ls_le [t_var v1; t_var x])
(f_app env.ls_le [t_var x; t_var v2]))
(wp_implies (wp_and (f_app le [t_var v1; t_var x])
(f_app le [t_var x; t_var v2]))
(wp_implies inv wp1)))
(let sv2 = t_app env.ls_add [t_var v2; t_int_const "1"] ty_int in
(let sv2 = t_app env.ls_add [t_var v2; incr] ty_int in
wp_implies (f_subst (subst1 x sv2) inv) q1)))
in
wp_and ~sym:true (wp_implies v1_gt_v2 q1) (wp_implies v1_le_v2 f)
......
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