Introducing Forr?! Forr? is a tiny language that translates to Boogie. The purpose of the language and verifier is to serve as a tutorial example for how to build a verifier on top of Boogie.

1 files changed, 39 insertions, 0 deletions

diff --git a/Test/forro/prog0.forro b/Test/forro/prog0.forro
new file mode 100644
index 00000000..87dbbd01
--- /dev/null
+++ b/Test/forro/prog0.forro
@@ -0,0 +1,39 @@
+procedure a b c := P x y z

+  requires 10

+  ensures 20

+do

+  if 30 then else end;

+  if 31 then else end;

+  while x < z

+    invariant x <= z

+    invariant b.valid and 1

+  do

+    k := x + 1;

+  end;

+  (x+5).head := c.tail;

+  a := new 17 18;

+  assert a != null;

+  m := k + a + null;

+  c := m;

+  call Q(x y y);

+  if x then

+    call a c b := P(a b c);

+  else

+    call R();

+  end;

+end;

+

+

+procedure Q x y z

+  requires 10

+  ensures 20

+do

+  if 40 then else end;

+end;

+

+

+procedure R

+  requires 10

+  ensures 20

+do

+end;