Nice view of guarantees ; add half test, proved.

1 files changed, 29 insertions, 0 deletions

diff --git a/tests/source/half.scade b/tests/source/half.scade
new file mode 100644
index 0000000..da90586
--- /dev/null
+++ b/tests/source/half.scade
@@ -0,0 +1,29 @@
+node test(i: int) returns (a, b, probe c: int; exit: bool)
+var
+  la, lb: int;
+  half: bool;
+let
+  exit = i >= 20;
+
+  half = true -> not pre half;
+
+  la = 0 -> pre a;
+  lb = 0 -> pre b;
+  activate
+    if half then
+      let
+        a = la + 1;
+        b = lb;
+      tel
+    else
+      let
+        a = la;
+        b = lb + 1;
+      tel
+  returns a, b;
+
+  c = a - b;
+
+  guarantee c_bounded: c >= 0 and c <= 1;
+  guarantee link_c_half: (half and c = 1) or ((not half) and c = 0);
+tel