diff options
author | 2010-11-17 17:31:39 +0000 | |
---|---|---|
committer | 2010-11-17 17:31:39 +0000 | |
commit | 9b2ab3b80a0c816862b8b6c90e64050b8369a51e (patch) | |
tree | e3d970800ca95f56e910da91ad4c7eaa6fde6e02 /Test/forro/prog0.forro | |
parent | 20ff8028079c6a7c5b4eb2999d1cad98c51ec5bb (diff) |
Forro: revised syntax (this version used in Boogie tutorial at SBMF 2010)
Diffstat (limited to 'Test/forro/prog0.forro')
-rw-r--r-- | Test/forro/prog0.forro | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Test/forro/prog0.forro b/Test/forro/prog0.forro index 87dbbd01..cf06e1f9 100644 --- a/Test/forro/prog0.forro +++ b/Test/forro/prog0.forro @@ -1,4 +1,4 @@ -procedure a b c := P x y z
+procedure a, b, c := P(x, y, z)
requires 10
ensures 20
do
@@ -11,20 +11,20 @@ do k := x + 1;
end;
(x+5).head := c.tail;
- a := new 17 18;
+ a := new (17, 18);
assert a != null;
m := k + a + null;
c := m;
- call Q(x y y);
+ call Q(x, y, y);
if x then
- call a c b := P(a b c);
+ call a, c, b := P(a, b, c);
else
call R();
end;
end;
-procedure Q x y z
+procedure Q(x, y, z)
requires 10
ensures 20
do
@@ -32,7 +32,7 @@ do end;
-procedure R
+procedure R()
requires 10
ensures 20
do
|