programs: syntax for infinite loops; rollback on the Init label

parent 27f869e9
......@@ -15,6 +15,7 @@ module HoareLogic
let slow_subtraction x z =
{ x >= 0 }
label Init:
while !x <> 0 do
invariant { 0 <= x and z - x = at z Init - at x Init } variant { x }
z := !z - 1;
......@@ -33,6 +34,7 @@ module HoareLogic
let slow_addition x z =
{ x >= 0 }
label Init:
while !x <> 0 do
invariant { 0 <= x and z + x = at z Init + at x Init } variant { x }
z := !z + 1;
......@@ -51,6 +53,7 @@ module HoareLogic
let parity x y =
{ x >= 0 }
y := 0;
label Init:
while !x <> 0 do
invariant { 0 <= x and (y=0 and even (at x Init - x) or
y=1 and even (at x Init - x + 1)) }
......@@ -109,6 +112,7 @@ module MoreHoareLogic
let list_sum l y =
{}
y := 0;
label Init:
while !l <> Nil do
invariant { length l <= length (at l Init) and
y + sum l = sum (at l Init) }
......@@ -125,6 +129,7 @@ module MoreHoareLogic
let list_member (x : ref (list 'a)) y z =
{}
z := 0;
label Init:
while !x <> Nil do
invariant { length x <= length (at x Init) and
(mem y x -> mem y (at x Init)) and
......
......@@ -1075,6 +1075,8 @@ expr:
{ mk_expr (Ematch (mk_expr (Etuple ($2::$4)), $7)) }
| LABEL uident COLON expr
{ mk_expr (Elabel ($2, $4)) }
| DO loop_annotation expr DONE
{ mk_expr (Eloop ($2, $3)) }
| WHILE expr DO loop_annotation expr DONE
{ mk_expr
(Etry
......@@ -1103,9 +1105,9 @@ expr:
triple:
| pre expr post
{ $1, add_init_label $2, $3 }
{ $1, (* add_init_label *) $2, $3 }
| expr %prec prec_triple
{ mk_pp PPtrue, add_init_label $1, (mk_pp PPtrue, []) }
{ mk_pp PPtrue, (* add_init_label *) $1, (mk_pp PPtrue, []) }
;
simple_expr:
......
......@@ -15,6 +15,17 @@ module P
end
{ r > old r }
exception Exit int
let foo () =
{}
let x = ref 0 in
do
x := !x + 1;
if !x = 100 then raise (Exit !x)
done
{ false } | Exit -> { result = 100 }
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