diff options
Diffstat (limited to 'Test/test2/Axioms.bpl')
-rw-r--r-- | Test/test2/Axioms.bpl | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/Test/test2/Axioms.bpl b/Test/test2/Axioms.bpl new file mode 100644 index 00000000..4fe7a8a7 --- /dev/null +++ b/Test/test2/Axioms.bpl @@ -0,0 +1,29 @@ +const Seven: int;
+axiom Seven == 7;
+
+function inc(int) returns (int);
+axiom (forall j: int :: inc(j) == j+1);
+
+procedure P()
+{
+ start:
+ assert 4 <= Seven;
+ assert Seven < inc(Seven);
+ assert inc(5) + inc(inc(2)) == Seven + 3;
+ return;
+}
+
+procedure Q()
+{
+ start:
+ assert inc(5) + inc(inc(2)) == Seven; // error
+ return;
+}
+
+function inc2(x:int) returns(int) { x + 2 }
+
+procedure ExpandTest()
+{
+ var q:int;
+ assert inc(inc(q)) == inc2(q);
+}
|