Permalink
Browse files

Add presentation sample demo.ww for regression test

  • Loading branch information...
1 parent f6b42fb commit 65e9d34628cf59a60b8f1ce57d5c6c0934aa87e6 @bafain bafain committed Mar 12, 2012
@@ -72,7 +72,7 @@
"smtlib-keywords", "test-qexpr-condition", "test-github-issue-93", "test-fibonacci",
"bubblesort2", "multiplication", "test-github-issue-108", "array_max",
"invalid_array_max", "test-valid-functioncall", "test-divisionbyzero-loopcondition",
- "array_min" };
+ "array_min", "demo", "demo_invalid" };
for (final String fileName : testPrograms) {
// Load test program and look for EXPECTED:???
@@ -0,0 +1,24 @@
+// EXPECTED:VALID
+/**
+ * Multiplies two numbers.
+ */
+function Integer mult(Integer i1, Integer i2)
+ _requires i1 ≥ 0
+ _ensures _return = i1 ⋅ i2
+{
+ Integer result := 0
+ Integer i := 0
+
+ while (i < i1)
+ _invariant i ≤ i1
+ _invariant result = i ⋅ i2
+ {
+ result := result + i2
+ i := i + 1
+ }
+
+ return result
+}
+
+Integer test := mult(2, 42)
+_assert test = 84
@@ -0,0 +1,23 @@
+// EXPECTED:INVALID
+/**
+ * Multiplies two numbers.
+ */
+function Integer mult(Integer i1, Integer i2)
+ _ensures _return = i1 ⋅ i2
+{
+ Integer result := 0
+ Integer i := 0
+
+ while (i < i1)
+ _invariant i ≤ i1
+ _invariant result = i ⋅ i2
+ {
+ result := result + i2
+ i := i + 1
+ }
+
+ return result
+}
+
+Integer test := mult(-2, 42)
+_assert test = -84
@@ -62,7 +62,7 @@
"smtlib-keywords", "test-qexpr-condition", "test-github-issue-93", "test-fibonacci",
"bubblesort2", "multiplication", "test-github-issue-108", "array_max",
"invalid_array_max", "test-valid-functioncall", "test-divisionbyzero-loopcondition",
- "array_min" };
+ "array_min", "demo", "demo_invalid" };
for (String fileName : testPrograms) {
// Load test program and look for EXPECTED:???
@@ -0,0 +1,24 @@
+// EXPECTED:VALID
+/**
+ * Multiplies two numbers.
+ */
+function Integer mult(Integer i1, Integer i2)
+ _requires i1 ≥ 0
+ _ensures _return = i1 ⋅ i2
+{
+ Integer result := 0
+ Integer i := 0
+
+ while (i < i1)
+ _invariant i ≤ i1
+ _invariant result = i ⋅ i2
+ {
+ result := result + i2
+ i := i + 1
+ }
+
+ return result
+}
+
+Integer test := mult(2, 42)
+_assert test = 84
@@ -0,0 +1,23 @@
+// EXPECTED:INVALID
+/**
+ * Multiplies two numbers.
+ */
+function Integer mult(Integer i1, Integer i2)
+ _ensures _return = i1 ⋅ i2
+{
+ Integer result := 0
+ Integer i := 0
+
+ while (i < i1)
+ _invariant i ≤ i1
+ _invariant result = i ⋅ i2
+ {
+ result := result + i2
+ i := i + 1
+ }
+
+ return result
+}
+
+Integer test := mult(-2, 42)
+_assert test = -84

0 comments on commit 65e9d34

Please sign in to comment.