diff options
Diffstat (limited to 'Test')
39 files changed, 719 insertions, 172 deletions
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy index 2a262d70..0f7c50c1 100644 --- a/Test/VSComp2010/Problem2-Invert.dfy +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -43,6 +43,7 @@ method M(N: int, A: array<int>, B: array<int>) assert (forall i :: 0 <= i && i < N ==> A[i] == old(A[i])); // the elements of A were not changed by the loop
// it now follows from the surjectivity of A that A is the inverse of B:
assert (forall j :: 0 <= j && j < N && inImage(j) ==> 0 <= B[j] && B[j] < N && A[B[j]] == j);
+ assert (forall j,k :: 0 <= j && j < k && k < N ==> B[j] != B[k]);
}
static function inImage(i: int): bool { true } // this function is used to trigger the surjective quantification
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer index 73a9509c..fe848aab 100644 --- a/Test/aitest0/Answer +++ b/Test/aitest0/Answer @@ -23,29 +23,29 @@ implementation Join(b: bool) x := 3;
y := 4;
z := x + y;
- assume {:inferred} x == 3 && y == 4 && z == 7;
- goto Then, Else;
+ assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7;
+ goto Then, Else;
Then:
- assume {:inferred} x == 3 && y == 4 && z == 7;
+ assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7;
assume b <==> true;
x := x + 1;
- assume {:inferred} x == 4 && y == 4 && z == 7;
+ assume {:inferred} GlobalFlag && x == 4 && y == 4 && z == 7 && b;
goto join;
Else:
- assume {:inferred} x == 3 && y == 4 && z == 7;
+ assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7;
assume b <==> false;
y := 4;
- assume {:inferred} x == 3 && y == 4 && z == 7;
+ assume {:inferred} GlobalFlag && x == 3 && y == 4 && z == 7 && !b;
goto join;
join:
- assume {:inferred} y == 4 && z == 7;
+ assume {:inferred} GlobalFlag && 3 <= x && x < 5 && y == 4 && z == 7;
assert y == 4;
assert z == 7;
assert GlobalFlag <==> true;
- assume {:inferred} y == 4 && z == 7;
+ assume {:inferred} GlobalFlag && 3 <= x && x < 5 && y == 4 && z == 7;
return;
}
@@ -68,20 +68,20 @@ implementation Loop() goto test;
test: // cut point
- assume {:inferred} c == 0;
- assume {:inferred} c == 0;
+ assume {:inferred} c == 0 && 0 <= i && i < 11;
+ assume {:inferred} c == 0 && 0 <= i && i < 11;
goto Then, Else;
Then:
- assume {:inferred} c == 0;
+ assume {:inferred} c == 0 && 0 <= i && i < 11;
assume i < 10;
i := i + 1;
- assume {:inferred} c == 0;
+ assume {:inferred} c == 0 && 1 <= i && i < 11;
goto test;
Else:
- assume {:inferred} c == 0;
- assume {:inferred} c == 0;
+ assume {:inferred} c == 0 && 0 <= i && i < 11;
+ assume {:inferred} c == 0 && 0 <= i && i < 11;
return;
}
diff --git a/Test/aitest0/runtest.bat b/Test/aitest0/runtest.bat index 1cb7a60c..b6ab77f0 100644 --- a/Test/aitest0/runtest.bat +++ b/Test/aitest0/runtest.bat @@ -3,5 +3,5 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-%BGEXE% %* -infer:c -instrumentInfer:e -printInstrumented -noVerify constants.bpl
+%BGEXE% %* -infer:j -instrumentInfer:e -printInstrumented -noVerify constants.bpl
%BGEXE% %* -infer:j Intervals.bpl
diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer index 718e7171..bfe185e7 100644 --- a/Test/aitest1/Answer +++ b/Test/aitest1/Answer @@ -14,21 +14,21 @@ implementation SimpleLoop() goto test;
test: // cut point
- assume {:inferred} 0 <= i;
- assume {:inferred} 0 <= i;
+ assume {:inferred} 0 <= i && i < 11;
+ assume {:inferred} 0 <= i && i < 11;
goto Then, Else;
Then:
- assume {:inferred} 0 <= i;
+ assume {:inferred} 0 <= i && i < 11;
assume i < 10;
i := i + 1;
- assume {:inferred} i <= 10 && 1 <= i;
+ assume {:inferred} 1 <= i && i < 11;
goto test;
Else:
- assume {:inferred} 0 <= i;
+ assume {:inferred} 0 <= i && i < 11;
assume !(i < 10);
- assume {:inferred} 10 <= i;
+ assume {:inferred} 0 <= i && i < 11;
return;
}
@@ -57,13 +57,13 @@ implementation VariableBoundLoop(n: int) assume {:inferred} 0 <= i;
assume i < n;
i := i + 1;
- assume {:inferred} i <= n && 1 <= i;
+ assume {:inferred} 1 <= i && 1 <= n;
goto test;
Else:
assume {:inferred} 0 <= i;
assume !(i < n);
- assume {:inferred} n <= i && 0 <= i;
+ assume {:inferred} 0 <= i;
return;
}
@@ -104,7 +104,7 @@ implementation FooToo() i := 3 * (i + 1);
i := 1 + 3 * i;
i := (i + 1) * 3;
- assume {:inferred} 1 / 3 * i == 155;
+ assume {:inferred} i == 465;
return;
}
@@ -125,7 +125,7 @@ implementation FooTooStepByStep() i := 3 * (i + 1);
i := 1 + 3 * i;
i := (i + 1) * 3;
- assume {:inferred} 1 / 3 * i == 155;
+ assume {:inferred} i == 465;
return;
}
@@ -212,7 +212,7 @@ implementation p() start:
assume {:inferred} true;
assume x < y;
- assume {:inferred} x + 1 <= y;
+ assume {:inferred} true;
return;
}
@@ -235,18 +235,18 @@ implementation p() A:
assume {:inferred} true;
assume x < y;
- assume {:inferred} x + 1 <= y;
+ assume {:inferred} true;
goto B, C;
B:
- assume {:inferred} x + 1 <= y;
+ assume {:inferred} true;
x := x * x;
assume {:inferred} true;
return;
C:
- assume {:inferred} x + 1 <= y;
- assume {:inferred} x + 1 <= y;
+ assume {:inferred} true;
+ assume {:inferred} true;
return;
}
@@ -268,26 +268,26 @@ implementation p() A:
assume {:inferred} true;
- assume 0 - 1 <= x;
+ assume -1 <= x;
assume {:inferred} -1 <= x;
goto B, E;
B:
assume {:inferred} -1 <= x;
assume x < y;
- assume {:inferred} x + 1 <= y && -1 <= x;
+ assume {:inferred} -1 <= x && 0 <= y;
goto C, E;
C:
- assume {:inferred} x + 1 <= y && -1 <= x;
+ assume {:inferred} -1 <= x && 0 <= y;
x := x * x;
- assume {:inferred} 0 <= y;
+ assume {:inferred} x < 2 && 0 <= y;
goto D, E;
D:
- assume {:inferred} 0 <= y;
+ assume {:inferred} x < 2 && 0 <= y;
x := y;
- assume {:inferred} x == y && 0 <= y;
+ assume {:inferred} 0 <= x && 0 <= y;
return;
E:
@@ -333,8 +333,8 @@ implementation p() goto D;
D:
- assume {:inferred} 9 <= x && x <= 10;
- assume {:inferred} 9 <= x && x <= 10;
+ assume {:inferred} 9 <= x && x < 11;
+ assume {:inferred} 9 <= x && x < 11;
return;
}
@@ -363,13 +363,13 @@ implementation p() B:
assume {:inferred} true;
assume x <= 0;
- assume {:inferred} x <= 0;
+ assume {:inferred} x < 1;
goto D;
C:
assume {:inferred} true;
assume y <= 0;
- assume {:inferred} y <= 0;
+ assume {:inferred} y < 1;
goto D;
D:
@@ -402,7 +402,7 @@ implementation foo() i := i + 1;
i := i + 1;
j := j + 1;
- assume {:inferred} i == j + 4 && j == 1 && n == 0;
+ assume {:inferred} i == 5 && j == 1 && n == 0;
return;
}
@@ -425,20 +425,20 @@ implementation foo() assume n >= 4;
i := 0;
j := i + 1;
- assume {:inferred} j == i + 1 && i == 0 && 4 <= n;
+ assume {:inferred} i == 0 && j == 1 && 4 <= n;
goto exit, loop0;
loop0: // cut point
- assume {:inferred} 4 <= n && 0 <= i && j == i + 1;
+ assume {:inferred} 0 <= i && 1 <= j && 4 <= n;
assume j <= n;
i := i + 1;
j := j + 1;
- assume {:inferred} j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;
+ assume {:inferred} 1 <= i && 2 <= j && 4 <= n;
goto loop0, exit;
exit:
- assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
- assume {:inferred} j <= n + 1 && 4 <= n && 0 <= i && j == i + 1;
+ assume {:inferred} 0 <= i && 1 <= j && 4 <= n;
+ assume {:inferred} 0 <= i && 1 <= j && 4 <= n;
return;
}
@@ -446,5 +446,10 @@ implementation foo() Boogie program verifier finished with 0 verified, 0 errors
-------------------- Bound.bpl --------------------
+Bound.bpl(24,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Bound.bpl(8,1): start
+ Bound.bpl(14,1): LoopHead
+ Bound.bpl(22,1): AfterLoop
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/aitest1/runtest.bat b/Test/aitest1/runtest.bat index 3b2c382c..6e8a7bb1 100644 --- a/Test/aitest1/runtest.bat +++ b/Test/aitest1/runtest.bat @@ -7,11 +7,11 @@ for %%f in (ineq.bpl Linear0.bpl Linear1.bpl Linear2.bpl Linear3.bpl Linear4.bpl Linear5.bpl Linear6.bpl
Linear7.bpl Linear8.bpl Linear9.bpl) do (
echo -------------------- %%f --------------------
- %BGEXE% %* -infer:p -instrumentInfer:e -printInstrumented -noVerify %%f
+ %BGEXE% %* -infer:j -instrumentInfer:e -printInstrumented -noVerify %%f
)
for %%f in (Bound.bpl) do (
echo -------------------- %%f --------------------
- %BGEXE% %* -infer:p %%f
+ %BGEXE% %* -infer:j %%f
)
diff --git a/Test/aitest9/runtest.bat b/Test/aitest9/runtest.bat index bafa6961..e66f7e2b 100644 --- a/Test/aitest9/runtest.bat +++ b/Test/aitest9/runtest.bat @@ -7,5 +7,5 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe for %%f in (VarMapFixPoint.bpl TestIntervals.bpl) do (
echo.
echo -------------------- %%f --------------------
- %BPLEXE% %* %%f /infer:i
+ %BPLEXE% %* %%f /infer:j
)
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 671c7c91..140f642f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -332,10 +332,10 @@ Execution trace: Definedness.dfy(86,5): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Definedness.dfy(86,10): Error: target object may be null
Execution trace:
(0,0): anon0
-Definedness.dfy(86,10): Error: target object may be null
+Definedness.dfy(86,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
Definedness.dfy(87,10): Error: possible violation of function precondition
@@ -542,7 +542,16 @@ ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specificat ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-48 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(363,4): Error: arguments to + must be int or a collection type (instead got bool)
+ResolutionErrors.dfy(368,4): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(371,4): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(371,4): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(372,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(372,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(377,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(377,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(382,4): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+57 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -553,7 +562,13 @@ ParseErrors.dfy(15,18): error: this operator cannot be part of a chain ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
-8 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(46,8): error: the main operator of a calculation must be transitive
+ParseErrors.dfy(62,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(63,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(68,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(69,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(75,2): error: this operator cannot continue this calculation
+14 parse errors detected in ParseErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
@@ -857,19 +872,19 @@ Execution trace: Dafny program verifier finished with 32 verified, 11 errors
-------------------- ControlStructures.dfy --------------------
-ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
+ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
- (0,0): anon8_Else
- (0,0): anon9_Then
-ControlStructures.dfy(5,3): Error: missing case in case statement: Purple
+ (0,0): anon8_Then
+ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
- (0,0): anon8_Then
+ (0,0): anon8_Else
+ (0,0): anon9_Then
ControlStructures.dfy(14,3): Error: missing case in case statement: Purple
Execution trace:
(0,0): anon0
@@ -1305,7 +1320,7 @@ CoPredicates.dfy(30,22): Related location: Related location Execution trace:
(0,0): anon0
-Dafny program verifier finished with 14 verified, 1 error
+Dafny program verifier finished with 12 verified, 1 error
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
@@ -1615,6 +1630,25 @@ TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive met TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods
5 resolution/type errors detected in TailCalls.dfy
+-------------------- Calculations.dfy --------------------
+Calculations.dfy(3,4): Error: index out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+Calculations.dfy(8,13): Error: index out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+Calculations.dfy(8,17): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+Calculations.dfy(36,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Calculations.dfy(31,2): anon5_Else
+
+Dafny program verifier finished with 4 verified, 4 errors
-------------------- IteratorResolution.dfy --------------------
IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field
IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy new file mode 100644 index 00000000..9e44f62e --- /dev/null +++ b/Test/dafny0/Calculations.dfy @@ -0,0 +1,37 @@ +method CalcTest0(s: seq<int>) { + calc { + s[0]; // error: ill-formed line + } + + calc { + 2; + { assert s[0] == 1; } // error: ill-formed hint + 1 + 1; + } + + if (|s| > 0) { + calc { + s[0]; // OK: well-formed in this context + { assert s[0] == s[0]; } + <= s[0]; + } + } +} + +method CalcTest1(x: int, y: int) { + calc { + x + y; + { assume x == 0; } + y; + } + assert x == 0; // OK: follows from x + y == y; +} + +method CalcTest2(x: int, y: int) { + calc { + x + y; + { assume x == 0; } + y + x; + } + assert x == 0; // error: even though assumed above, is not exported by the calculation +}
\ No newline at end of file diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy index 67dff91b..c5651c90 100644 --- a/Test/dafny0/CoPredicates.dfy +++ b/Test/dafny0/CoPredicates.dfy @@ -51,8 +51,9 @@ function U2(n: int): Stream<int> UpwardBy2(n)
}
-ghost method Lemma2(n: int)
- ensures Even(UpwardBy2(2*n)); // this is true, but Dafny can't prove it
-{
- assert Even(U2(2*n)); // ... thanks to this lemma
-}
+// Postponed:
+//ghost method Lemma2(n: int)
+// ensures Even(UpwardBy2(2*n)); // this is true, and Dafny can prove it
+//{
+// assert Even(U2(2*n)); // ... thanks to this lemma
+//}
diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy index 41df50eb..9a3cc18b 100644 --- a/Test/dafny0/ParseErrors.dfy +++ b/Test/dafny0/ParseErrors.dfy @@ -18,3 +18,61 @@ method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set ensures x in s == t; // error: 'in' is not chaining
{
}
+
+// ---------------------- calc statements -----------------------------------
+
+method TestCalc()
+{
+ calc {} // OK, empty calculations are allowed
+ calc {
+ 2 + 3; // OK, single-line calculations are allowed
+ }
+ calc {
+ 2 + 3;
+ calc { // OK: a calc statement is allowed as a sub-hint
+ 2;
+ 1 + 1;
+ }
+ calc {
+ 3;
+ 1 + 2;
+ }
+ { assert true; } // OK: multiple subhints are allowed between two lines
+ 1 + 1 + 1 + 2;
+ { assert 1 + 1 + 1 == 3; }
+ { assert true; }
+ 3 + 2;
+ }
+ calc != { // error: != is not allowed as the main operator of a calculation
+ 2 + 3;
+ 4;
+ }
+ calc { // OK, these operators are compatible
+ 2 + 3;
+ > 4;
+ >= 2 + 2;
+ }
+ calc < { // OK, these operators are compatible
+ 2 + 3;
+ == 5;
+ <= 3 + 3;
+ }
+ calc < { // error: cannot mix < and >= or >
+ 2 + 3;
+ >= 5;
+ > 2 + 2;
+ 6;
+ }
+ calc >= { // error: cannot mix >= and <= or !=
+ 2 + 3;
+ <= 5;
+ != 2 + 2;
+ 3;
+ }
+ calc { // error: cannot have more than one != per calc
+ 2 + 3;
+ != 4;
+ != 1 + 2;
+ 3;
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 274cc95a..c615c5ec 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -354,3 +354,32 @@ method MG1(l: GList, n: nat) var t := GCons(100, GNil);
t := GCons(120, l); // error: types don't match up (List<T$0> versus List<int>)
}
+
+// ------------------- calc statements ------------------------------
+
+method TestCalc(m: int, n: int, a: bool, b: bool)
+{
+ calc {
+ a + b; // error: invalid line
+ n + m;
+ }
+ calc {
+ a && b;
+ n + m; // error: all lines must have the same type
+ }
+ calc ==> {
+ n + m; // error: ==> operator requires boolean lines
+ n + m + 1;
+ n + m + 2;
+ }
+ calc {
+ n + m;
+ n + m + 1;
+ ==> n + m + 2; // error: ==> operator requires boolean lines
+ }
+ calc {
+ n + m;
+ { print n + m; } // error: non-ghost statements are not allowed in hints
+ m + n;
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 9789e7d7..9118e388 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -24,7 +24,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy
RefinementModificationChecking.dfy TailCalls.dfy
- IteratorResolution.dfy Iterators.dfy) do (
+ Calculations.dfy IteratorResolution.dfy Iterators.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index 447f4365..2feaf6f7 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -54,3 +54,7 @@ Dafny program verifier finished with 3 verified, 0 errors -------------------- MonotonicHeapstate.dfy --------------------
Dafny program verifier finished with 36 verified, 0 errors
+
+-------------------- Calculations.dfy --------------------
+
+Dafny program verifier finished with 26 verified, 0 errors
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy new file mode 100644 index 00000000..8c13457b --- /dev/null +++ b/Test/dafny2/Calculations.dfy @@ -0,0 +1,209 @@ +/* Lists */
+// Here are some standard definitions of List and functions on Lists
+
+datatype List<T> = Nil | Cons(T, List);
+
+function length(l: List): nat
+{
+ match l
+ case Nil => 0
+ case Cons(x, xs) => 1 + length(xs)
+}
+
+function concat(l: List, ys: List): List
+{
+ match l
+ case Nil => ys
+ case Cons(x, xs) => Cons(x, concat(xs, ys))
+}
+
+function reverse(l: List): List
+{
+ match l
+ case Nil => Nil
+ case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil))
+}
+
+function revacc(l: List, acc: List): List
+{
+ match l
+ case Nil => acc
+ case Cons(x, xs) => revacc(xs, Cons(x, acc))
+}
+
+function qreverse(l: List): List
+{
+ revacc(l, Nil)
+}
+
+// Here are two lemmas about the List functions.
+
+ghost method Lemma_ConcatNil()
+ ensures forall xs :: concat(xs, Nil) == xs;
+{
+}
+
+ghost method Lemma_RevCatCommute()
+ ensures forall xs, ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);
+{
+}
+
+// Here is a theorem that says "qreverse" and "reverse" calculate the same result. The proof
+// is given in a calculational style. The proof is not minimal--some lines can be omitted
+// and Dafny will still fill in the details.
+
+ghost method Theorem_QReverseIsCorrect_Calc(l: List)
+ ensures qreverse(l) == reverse(l);
+{
+ calc {
+ qreverse(l);
+ // def. qreverse
+ revacc(l, Nil);
+ { Lemma_Revacc_calc(l, Nil); }
+ concat(reverse(l), Nil);
+ { Lemma_ConcatNil(); }
+ reverse(l);
+ }
+}
+
+ghost method Lemma_Revacc_calc(xs: List, ys: List)
+ ensures revacc(xs, ys) == concat(reverse(xs), ys);
+{
+ match (xs) {
+ case Nil =>
+ case Cons(x, xrest) =>
+ calc {
+ concat(reverse(xs), ys);
+ // def. reverse
+ concat(concat(reverse(xrest), Cons(x, Nil)), ys);
+ // induction hypothesis: Lemma_Revacc_calc(xrest, Cons(x, Nil))
+ concat(revacc(xrest, Cons(x, Nil)), ys);
+ { Lemma_RevCatCommute(); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
+ revacc(xrest, concat(Cons(x, Nil), ys));
+ // def. concat (x2)
+ revacc(xrest, Cons(x, ys));
+ // def. revacc
+ revacc(xs, ys);
+ }
+ }
+}
+
+// Here is a version of the same proof, as it was constructed before Dafny's "calc" construct.
+
+ghost method Theorem_QReverseIsCorrect(l: List)
+ ensures qreverse(l) == reverse(l);
+{
+ assert qreverse(l)
+ == // def. qreverse
+ revacc(l, Nil);
+ Lemma_Revacc(l, Nil);
+ assert revacc(l, Nil)
+ == concat(reverse(l), Nil);
+ Lemma_ConcatNil();
+}
+
+ghost method Lemma_Revacc(xs: List, ys: List)
+ ensures revacc(xs, ys) == concat(reverse(xs), ys);
+{
+ match (xs) {
+ case Nil =>
+ case Cons(x, xrest) =>
+ assert revacc(xs, ys)
+ == // def. revacc
+ revacc(xrest, Cons(x, ys));
+
+ assert concat(reverse(xs), ys)
+ == // def. reverse
+ concat(concat(reverse(xrest), Cons(x, Nil)), ys)
+ == // induction hypothesis: Lemma3a(xrest, Cons(x, Nil))
+ concat(revacc(xrest, Cons(x, Nil)), ys);
+ Lemma_RevCatCommute(); // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
+ assert concat(revacc(xrest, Cons(x, Nil)), ys)
+ == revacc(xrest, concat(Cons(x, Nil), ys));
+
+ assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
+
+ assert revacc(xrest, concat(Cons(x, Nil), ys))
+ == // the assert lemma just above
+ revacc(xrest, Cons(x, ys));
+ }
+}
+
+/* Fibonacci */
+// To further demonstrate what the "calc" construct can do, here are some proofs about the Fibonacci function.
+
+function Fib(n: nat): nat
+{
+ if n < 2 then n else Fib(n - 2) + Fib(n - 1)
+}
+
+ghost method Lemma_Fib()
+ ensures Fib(5) < 6;
+{
+ calc {
+ Fib(5);
+ Fib(4) + Fib(3);
+ calc {
+ Fib(2);
+ Fib(0) + Fib(1);
+ 0 + 1;
+ 1;
+ }
+ < 6;
+ }
+}
+
+/* List length */
+// Here are some proofs that show the use of nested calculations.
+
+ghost method Lemma_Concat_Length(xs: List, ys: List)
+ ensures length(concat(xs, ys)) == length(xs) + length(ys);
+{}
+
+ghost method Lemma_Reverse_Length(xs: List)
+ ensures length(xs) == length(reverse(xs));
+{
+ match (xs) {
+ case Nil =>
+ case Cons(x, xrest) =>
+ calc {
+ length(reverse(xs));
+ // def. reverse
+ length(concat(reverse(xrest), Cons(x, Nil)));
+ { Lemma_Concat_Length(reverse(xrest), Cons(x, Nil)); }
+ length(reverse(xrest)) + length(Cons(x, Nil));
+ // induction hypothesis
+ length(xrest) + length(Cons(x, Nil));
+ calc {
+ length(Cons(x, Nil));
+ // def. length
+ 1 + length(Nil);
+ // def. length
+ 1 + 0;
+ 1;
+ }
+ length(xrest) + 1;
+ // def. length
+ length(xs);
+ }
+ }
+}
+
+ghost method Window(xs: List, ys: List)
+ ensures length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(ys));
+{
+ calc {
+ length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(ys));
+ { if (length(xs) == length(ys)) {
+ calc {
+ length(reverse(xs));
+ { Lemma_Reverse_Length(xs); }
+ length(xs);
+ length(ys);
+ { Lemma_Reverse_Length(ys); }
+ length(reverse(ys));
+ } } }
+ length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(xs));
+ true;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 909f67f5..72959830 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -16,7 +16,7 @@ for %%f in ( StoreAndRetrieve.dfy
Intervals.dfy TreeFill.dfy TuringFactorial.dfy
MajorityVote.dfy SegmentSum.dfy
- MonotonicHeapstate.dfy
+ MonotonicHeapstate.dfy Calculations.dfy
) do (
echo.
echo -------------------- %%f --------------------
diff --git a/Test/inline/Answer b/Test/inline/Answer index 655143fa..eddeb64f 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -566,7 +566,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in var b: bool;
anon0:
- ret := 0 - 1;
+ ret := -1;
b := false;
found := b;
i := 0;
@@ -659,7 +659,7 @@ implementation main(x: int) goto inline$find$0$anon0;
inline$find$0$anon0:
- inline$find$0$ret := 0 - 1;
+ inline$find$0$ret := -1;
inline$find$0$b := false;
inline$find$0$found := inline$find$0$b;
inline$find$0$i := 0;
@@ -756,7 +756,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in var inline$check$0$ret: bool;
anon0:
- ret := 0 - 1;
+ ret := -1;
b := false;
found := b;
i := 0;
diff --git a/Test/livevars/bla1.bpl b/Test/livevars/bla1.bpl index 2854e5df..12ccc44a 100644 --- a/Test/livevars/bla1.bpl +++ b/Test/livevars/bla1.bpl @@ -471,7 +471,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y}
function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y}
function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y}
-function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y}
+function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y}
function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y}
diff --git a/Test/livevars/daytona_bug2_ioctl_example_1.bpl b/Test/livevars/daytona_bug2_ioctl_example_1.bpl index 1decba12..ae8ff08c 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_1.bpl +++ b/Test/livevars/daytona_bug2_ioctl_example_1.bpl @@ -510,7 +510,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y}
function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y}
function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y}
-function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y}
+function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y}
function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y}
diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl b/Test/livevars/daytona_bug2_ioctl_example_2.bpl index 0b49364b..44e51827 100644 --- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl +++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl @@ -521,7 +521,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y}
function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y}
function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y}
-function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y}
+function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y}
function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y}
diff --git a/Test/livevars/stack_overflow.bpl b/Test/livevars/stack_overflow.bpl index 242acd65..fae3e863 100644 --- a/Test/livevars/stack_overflow.bpl +++ b/Test/livevars/stack_overflow.bpl @@ -831,7 +831,7 @@ function {:inline true} INT_NEQ(x:int, y:int) returns (bool) {x != y} function {:inline true} INT_ADD(x:int, y:int) returns (int) {x + y}
function {:inline true} INT_SUB(x:int, y:int) returns (int) {x - y}
function {:inline true} INT_MULT(x:int, y:int) returns (int) {x * y}
-function {:inline true} INT_DIV(x:int, y:int) returns (int) {x / y}
+function {:inline true} INT_DIV(x:int, y:int) returns (int) {x div y}
function {:inline true} INT_LT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_ULT(x:int, y:int) returns (bool) {x < y}
function {:inline true} INT_LEQ(x:int, y:int) returns (bool) {x <= y}
diff --git a/Test/prover/Answer b/Test/prover/Answer index 1ca6407c..688e6e6a 100644 --- a/Test/prover/Answer +++ b/Test/prover/Answer @@ -4,7 +4,7 @@ z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(5,1): start
- z3mutl.bpl(14,1): L3
+ z3mutl.bpl(8,1): L1
z3mutl.bpl(20,1): L5
z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
@@ -14,7 +14,7 @@ Execution trace: z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(5,1): start
- z3mutl.bpl(8,1): L1
+ z3mutl.bpl(14,1): L3
z3mutl.bpl(20,1): L5
Boogie program verifier finished with 0 verified, 3 errors
@@ -24,19 +24,19 @@ EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hol EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.
Execution trace:
EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY
- EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2
EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2
- EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2
- EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2
EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2
EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hold on this return path.
EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.
Execution trace:
EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY
- EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2
EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2
- EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2
- EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2
EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2
EQ_v2.Eval__v4.Eval_out.bpl(2152,5): Error BP5003: A postcondition might not hold on this return path.
EQ_v2.Eval__v4.Eval_out.bpl(2120,3): Related location: This is the postcondition that might not hold.
diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl index e4da94f4..e53e00b4 100644 --- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl +++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl @@ -382,7 +382,7 @@ axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y);
-axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x / y);
+axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y);
axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y);
@@ -1173,7 +1173,7 @@ axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y);
-axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x / y);
+axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x div y);
axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y);
diff --git a/Test/test0/Answer b/Test/test0/Answer index 51a139b7..0eda9e2e 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -34,6 +34,12 @@ const y: int; const z: int;
+const r: real;
+
+const s: real;
+
+const t: real;
+
const P: bool;
const Q: bool;
@@ -48,10 +54,44 @@ axiom x * y * z == x * y * z; axiom x * y * z * x == x * y * z;
+axiom x div y div z == x div (y div z);
+
+axiom x div y div (z div x) == x div y div z;
+
+axiom x + y mod z == y mod z + x;
+
+axiom (x + y) mod z == x mod z + y mod z;
+
axiom x / y / z == x / (y / z);
axiom x / y / (z / x) == x / y / z;
+axiom x / s / z == x / (s / z);
+
+axiom x / s / (z / x) == x / s / z;
+
+axiom r / s / t == r / (s / t);
+
+axiom r / s / (t / r) == r / s / t;
+
+axiom r * s / t == r * s / t;
+
+axiom r / s * t == r / s * t;
+
+axiom (r * s) ** t == r ** t * s ** t;
+
+axiom r ** (s + t) == r ** s * r ** t;
+
+axiom int(real(x)) == x;
+
+axiom r >= 0e0 ==> real(int(r)) <= r;
+
+axiom int(0e0 - 2e-2) == 0;
+
+axiom int(0e0 - 35e0) == -35;
+
+axiom int(27e-1) == 2;
+
axiom x - y - z == x - (y - z);
axiom x - y - (z - x) == x - y - z;
diff --git a/Test/test0/BadLabels1.bpl b/Test/test0/BadLabels1.bpl index 28fb47b8..c040ce26 100644 --- a/Test/test0/BadLabels1.bpl +++ b/Test/test0/BadLabels1.bpl @@ -28,7 +28,7 @@ procedure P1(y: int) {
K:
goto A;
- if (y % 2 == 0) {
+ if (y mod 2 == 0) {
goto L;
M:
}
diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl index cb69aa5f..5fffc20a 100644 --- a/Test/test0/ModifiedBag.bpl +++ b/Test/test0/ModifiedBag.bpl @@ -1,5 +1,5 @@ // ----------- BEGIN PRELUDE
-type real;
+
type elements;
diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl index a1f941d8..7e4a9ce7 100644 --- a/Test/test0/PrettyPrint.bpl +++ b/Test/test0/PrettyPrint.bpl @@ -1,6 +1,9 @@ const x: int;
const y: int;
const z: int;
+const r: real;
+const s: real;
+const t: real;
const P: bool;
const Q: bool;
const R: bool;
@@ -11,8 +14,30 @@ axiom (x * y) + z == (x + y) * z; axiom x * y * z == (x * (y * z));
axiom (x * y) * (z * x) == (x * y) * z;
+axiom x div y div z == (x div (y div z));
+axiom (x div y) div (z div x) == (x div y) div z;
+
+axiom x + y mod z == ((y mod z) + x);
+axiom (x + y) mod z == (x mod z) + (y mod z);
+
axiom x / y / z == (x / (y / z));
axiom (x / y) / (z / x) == (x / y) / z;
+axiom x / s / z == (x / (s / z));
+axiom (x / s) / (z / x) == (x / s) / z;
+axiom r / s / t == (r / (s / t));
+axiom (r / s) / (t / r) == (r / s) / t;
+
+axiom ((r * s) / t) == r * s / t;
+axiom ((r / s) * t) == (r / s) * t;
+
+axiom (r * s) ** t == (r ** t) * (s ** t);
+axiom r ** (s + t) == r ** s * r ** t;
+
+axiom int(real(x)) == x;
+axiom r >= 0.0 ==> real(int(r)) <= r;
+axiom int(0e-3 - 0.02) == 0;
+axiom int(0e2 - 3.5e1) == -35;
+axiom int(27e-1) == 2;
axiom x - y - z == (x - (y - z));
axiom (x - y) - (z - x) == (x - y) - z;
diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl index ac87476f..79a4d2ab 100644 --- a/Test/test0/Prog0.bpl +++ b/Test/test0/Prog0.bpl @@ -1,5 +1,5 @@ // BoogiePL Examples
-type real;
+
type elements;
var x:int; var y:real; var z:ref; // Variables
diff --git a/Test/test1/Answer b/Test/test1/Answer index a8b73b53..94bf2d9a 100644 --- a/Test/test1/Answer +++ b/Test/test1/Answer @@ -145,3 +145,22 @@ Lambda.bpl(12,8): Error: the type variable T does not occur in types of the lamb Lambda.bpl(12,2): Error: mismatched types in assignment command (cannot assign <T>[int]int to [int]int)
Lambda.bpl(18,27): Error: invalid argument types (bool and int) to binary operator +
5 type checking errors detected in Lambda.bpl
+IntReal.bpl(5,8): Error: invalid argument types (int and real) to binary operator >=
+IntReal.bpl(6,8): Error: invalid argument types (int and real) to binary operator <=
+IntReal.bpl(7,8): Error: invalid argument types (int and real) to binary operator <
+IntReal.bpl(8,8): Error: invalid argument types (int and real) to binary operator >
+IntReal.bpl(10,9): Error: invalid argument types (int and real) to binary operator ==
+IntReal.bpl(11,8): Error: invalid argument types (int and real) to binary operator +
+IntReal.bpl(12,8): Error: invalid argument types (int and real) to binary operator -
+IntReal.bpl(13,8): Error: invalid argument types (int and real) to binary operator *
+IntReal.bpl(14,8): Error: invalid argument types (int and real) to binary operator div
+IntReal.bpl(15,8): Error: invalid argument types (int and real) to binary operator mod
+IntReal.bpl(17,12): Error: invalid argument types (real and int) to binary operator ==
+IntReal.bpl(23,8): Error: invalid argument types (int and real) to binary operator **
+IntReal.bpl(27,14): Error: invalid argument types (real and int) to binary operator ==
+IntReal.bpl(29,13): Error: invalid argument types (int and real) to binary operator ==
+IntReal.bpl(32,6): Error: argument type int does not match expected type real
+IntReal.bpl(33,6): Error: argument type real does not match expected type int
+IntReal.bpl(45,8): Error: invalid argument types (real and int) to binary operator div
+IntReal.bpl(46,8): Error: invalid argument types (real and int) to binary operator mod
+18 type checking errors detected in IntReal.bpl
\ No newline at end of file diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl new file mode 100644 index 00000000..976fc864 --- /dev/null +++ b/Test/test1/IntReal.bpl @@ -0,0 +1,48 @@ +const i: int;
+const r: real;
+
+axiom i == 0;
+axiom i >= 0.0; // type error
+axiom i <= 0.0e0; // type error
+axiom i < 0.0e-0; // type error
+axiom i > 0.0e20; // type error
+
+axiom -i == r; // type error
+axiom i + r == 0.0; // type error
+axiom i - r == 0.0; // type error
+axiom i * r == 0.0; // type error
+axiom i div r == 0; // type error
+axiom i mod r == 0; // type error
+
+axiom i / i == 0; // type error
+axiom i / i == 0.0;
+axiom i / r == 0.0;
+axiom r / i == 0.0;
+axiom r / r == 0.0;
+
+axiom i ** r == 0.0; // type error
+axiom r ** r == 0.0;
+
+axiom real(i) == 0.0;
+axiom real(i) == i; // type error
+axiom int(r) == 0;
+axiom int(r) == r; // type error
+axiom int(real(i)) == i;
+axiom real(int(r)) == r;
+axiom int(int(r)) == i; // type error
+axiom real(real(i)) == r; // type error
+
+axiom i == 0;
+axiom real(i) >= 0.0;
+axiom real(i) <= 0.0e0;
+axiom r < 0.0e-0;
+axiom r > 0.0e20;
+
+axiom -r == real(i);
+axiom real(i) + r == 0.0;
+axiom r - real(0) == 0.0;
+axiom r * r == 0.0;
+axiom r div 0 == 0; // type error
+axiom r mod 0 == 0; // type error
+
+axiom r ** r == 0.0;
diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat index 979c36e4..149e6dc9 100644 --- a/Test/test1/runtest.bat +++ b/Test/test1/runtest.bat @@ -19,3 +19,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe %BGEXE% %* /noVerify FunBody.bpl
%BGEXE% %* /noVerify IfThenElse0.bpl
%BGEXE% %* /noVerify Lambda.bpl
+%BGEXE% %* /noVerify IntReal.bpl
diff --git a/Test/test15/Answer b/Test/test15/Answer index 3361b320..915f63e8 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -1,22 +1,24 @@ -------------------- NullInModel --------------------
*** MODEL
-%lbl%@46 -> false
-%lbl%+23 -> true
-%lbl%+36 -> true
-boolType -> T@T!val!1
+%lbl%@45 -> false
+%lbl%+24 -> true
+%lbl%+35 -> true
+boolType -> T@T!val!2
intType -> T@T!val!0
null -> T@U!val!0
-refType -> T@T!val!2
+realType -> T@T!val!1
+refType -> T@T!val!3
s -> T@U!val!0
type -> {
- T@U!val!0 -> T@T!val!2
- else -> T@T!val!2
+ T@U!val!0 -> T@T!val!3
+ else -> T@T!val!3
}
Ctor -> {
T@T!val!0 -> 0
T@T!val!1 -> 1
T@T!val!2 -> 2
+ T@T!val!3 -> 3
else -> 0
}
tickleBool -> {
@@ -33,15 +35,17 @@ Boogie program verifier finished with 0 verified, 1 error -------------------- IntInModel --------------------
*** MODEL
-%lbl%@38 -> false
-%lbl%+22 -> true
-%lbl%+28 -> true
-boolType -> T@T!val!1
+%lbl%@37 -> false
+%lbl%+23 -> true
+%lbl%+27 -> true
+boolType -> T@T!val!2
i -> 0
intType -> T@T!val!0
+realType -> T@T!val!1
Ctor -> {
T@T!val!0 -> 0
T@T!val!1 -> 1
+ T@T!val!2 -> 2
else -> 0
}
tickleBool -> {
@@ -58,27 +62,29 @@ Boogie program verifier finished with 0 verified, 1 error -------------------- ModelTest --------------------
*** MODEL
-%lbl%@181 -> false
-%lbl%+118 -> true
-%lbl%+63 -> true
-boolType -> T@T!val!1
+%lbl%@145 -> false
+%lbl%+64 -> true
+%lbl%+82 -> true
+boolType -> T@T!val!2
i@0 -> 1
intType -> T@T!val!0
j@0 -> 2
j@1 -> 3
j@2 -> 4
r -> T@U!val!1
-refType -> T@T!val!2
+realType -> T@T!val!1
+refType -> T@T!val!3
s -> T@U!val!0
type -> {
- T@U!val!0 -> T@T!val!2
- T@U!val!1 -> T@T!val!2
- else -> T@T!val!2
+ T@U!val!0 -> T@T!val!3
+ T@U!val!1 -> T@T!val!3
+ else -> T@T!val!3
}
Ctor -> {
T@T!val!0 -> 0
T@T!val!1 -> 1
T@T!val!2 -> 2
+ T@T!val!3 -> 3
else -> 0
}
tickleBool -> {
@@ -114,37 +120,38 @@ Execution trace: CaptureState.bpl(16,5): anon4_Then
CaptureState.bpl(24,5): anon3
*** MODEL
-%lbl%@335 -> false
-%lbl%+111 -> true
-%lbl%+113 -> true
-%lbl%+117 -> true
-%lbl%+190 -> true
+%lbl%@291 -> false
+%lbl%+112 -> true
+%lbl%+114 -> true
+%lbl%+118 -> true
+%lbl%+146 -> true
@MV_state_const -> 6
-boolType -> T@T!val!1
+boolType -> T@T!val!2
F -> T@U!val!2
-FieldNameType -> T@T!val!3
+FieldNameType -> T@T!val!4
Heap -> T@U!val!0
intType -> T@T!val!0
m -> **m
-m@0 -> -2
-m@2 -> -1
-m@3 -> -1
+m@0 -> -451
+m@2 -> -450
+m@3 -> -450
r -> **r
-r@0 -> -2
-RefType -> T@T!val!2
+r@0 -> -900
+realType -> T@T!val!1
+RefType -> T@T!val!3
this -> T@U!val!1
-x@@4 -> 797
+x@@5 -> 0
y@@1 -> **y@@1
int_2_U -> {
- -2 -> -2
- else -> -2
+ -451 -> -451
+ else -> -451
}
type -> {
- T@U!val!0 -> T@T!val!4
- T@U!val!1 -> T@T!val!2
- T@U!val!2 -> T@T!val!3
- -2 -> T@T!val!0
- else -> T@T!val!4
+ T@U!val!0 -> T@T!val!5
+ T@U!val!1 -> T@T!val!3
+ T@U!val!2 -> T@T!val!4
+ -451 -> T@T!val!0
+ else -> T@T!val!5
}
@MV_state -> {
6 0 -> true
@@ -156,26 +163,27 @@ type -> { Ctor -> {
T@T!val!0 -> 0
T@T!val!1 -> 1
- T@T!val!2 -> 3
+ T@T!val!2 -> 2
T@T!val!3 -> 4
- T@T!val!4 -> 2
+ T@T!val!4 -> 5
+ T@T!val!5 -> 3
else -> 0
}
[3] -> {
- T@U!val!0 T@U!val!1 T@U!val!2 -> -2
- else -> -2
+ T@U!val!0 T@U!val!1 T@U!val!2 -> -451
+ else -> -451
}
U_2_int -> {
- -2 -> -2
- else -> -2
+ -451 -> -451
+ else -> -451
}
MapType0TypeInv1 -> {
- T@T!val!4 -> T@T!val!3
- else -> T@T!val!3
+ T@T!val!5 -> T@T!val!4
+ else -> T@T!val!4
}
MapType0TypeInv0 -> {
- T@T!val!4 -> T@T!val!2
- else -> T@T!val!2
+ T@T!val!5 -> T@T!val!3
+ else -> T@T!val!3
}
tickleBool -> {
true -> true
@@ -183,17 +191,17 @@ tickleBool -> { else -> true
}
MapType0Type -> {
- T@T!val!2 T@T!val!3 T@T!val!0 -> T@T!val!4
- else -> T@T!val!4
+ T@T!val!3 T@T!val!4 T@T!val!0 -> T@T!val!5
+ else -> T@T!val!5
}
MapType0TypeInv2 -> {
- T@T!val!4 -> T@T!val!0
+ T@T!val!5 -> T@T!val!0
else -> T@T!val!0
}
*** STATE <initial>
Heap -> T@U!val!0
this -> T@U!val!1
- x -> 797
+ x -> 0
y -> **y@@1
r -> **r
m -> **m
@@ -201,13 +209,13 @@ MapType0TypeInv2 -> { *** STATE top
*** END_STATE
*** STATE then
- m -> -2
+ m -> -451
*** END_STATE
*** STATE postUpdate0
- m -> -1
+ m -> -450
*** END_STATE
*** STATE end
- r -> -2
+ r -> -900
m -> 7
*** END_STATE
*** END_MODEL
diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl index ff723db2..6aee18ea 100644 --- a/Test/test2/strings-no-where.bpl +++ b/Test/test2/strings-no-where.bpl @@ -1,4 +1,4 @@ -type real;
+
type elements;
@@ -330,23 +330,23 @@ function #shl(int, int) returns (int); function #shr(int, int) returns (int);
-axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y);
+axiom (forall x: int, y: int :: { x mod y } { x div y } x mod y == x - x div y * y);
-axiom (forall x: int, y: int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y);
+axiom (forall x: int, y: int :: { x mod y } 0 <= x && 0 < y ==> 0 <= x mod y && x mod y < y);
-axiom (forall x: int, y: int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y);
+axiom (forall x: int, y: int :: { x mod y } 0 <= x && y < 0 ==> 0 <= x mod y && x mod y < 0 - y);
-axiom (forall x: int, y: int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0);
+axiom (forall x: int, y: int :: { x mod y } x <= 0 && 0 < y ==> 0 - y < x mod y && x mod y <= 0);
-axiom (forall x: int, y: int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0);
+axiom (forall x: int, y: int :: { x mod y } x <= 0 && y < 0 ==> y < x mod y && x mod y <= 0);
-axiom (forall x: int, y: int :: { (x + y) % y } 0 <= x && 0 <= y ==> (x + y) % y == x % y);
+axiom (forall x: int, y: int :: { (x + y) mod y } 0 <= x && 0 <= y ==> (x + y) mod y == x mod y);
-axiom (forall x: int, y: int :: { (y + x) % y } 0 <= x && 0 <= y ==> (y + x) % y == x % y);
+axiom (forall x: int, y: int :: { (y + x) mod y } 0 <= x && 0 <= y ==> (y + x) mod y == x mod y);
-axiom (forall x: int, y: int :: { (x - y) % y } 0 <= x - y && 0 <= y ==> (x - y) % y == x % y);
+axiom (forall x: int, y: int :: { (x - y) mod y } 0 <= x - y && 0 <= y ==> (x - y) mod y == x mod y);
-axiom (forall a: int, b: int, d: int :: { a % d,b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
+axiom (forall a: int, b: int, d: int :: { a mod d,b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b);
axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i);
@@ -354,7 +354,7 @@ axiom (forall i: int, j: int :: 0 <= j ==> #shl(i, j + 1) == #shl(i, j) * 2); axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i);
-axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) / 2);
+axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) div 2);
const unique $UnknownRef: ref;
diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl index da529b84..f196899f 100644 --- a/Test/test2/strings-where.bpl +++ b/Test/test2/strings-where.bpl @@ -1,4 +1,4 @@ -type real;
+
type elements;
@@ -330,23 +330,23 @@ function #shl(int, int) returns (int); function #shr(int, int) returns (int);
-axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y);
+axiom (forall x: int, y: int :: { x mod y } { x div y } x mod y == x - x div y * y);
-axiom (forall x: int, y: int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y);
+axiom (forall x: int, y: int :: { x mod y } 0 <= x && 0 < y ==> 0 <= x mod y && x mod y < y);
-axiom (forall x: int, y: int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y);
+axiom (forall x: int, y: int :: { x mod y } 0 <= x && y < 0 ==> 0 <= x mod y && x mod y < 0 - y);
-axiom (forall x: int, y: int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0);
+axiom (forall x: int, y: int :: { x mod y } x <= 0 && 0 < y ==> 0 - y < x mod y && x mod y <= 0);
-axiom (forall x: int, y: int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0);
+axiom (forall x: int, y: int :: { x mod y } x <= 0 && y < 0 ==> y < x mod y && x mod y <= 0);
-axiom (forall x: int, y: int :: { (x + y) % y } 0 <= x && 0 <= y ==> (x + y) % y == x % y);
+axiom (forall x: int, y: int :: { (x + y) mod y } 0 <= x && 0 <= y ==> (x + y) mod y == x mod y);
-axiom (forall x: int, y: int :: { (y + x) % y } 0 <= x && 0 <= y ==> (y + x) % y == x % y);
+axiom (forall x: int, y: int :: { (y + x) mod y } 0 <= x && 0 <= y ==> (y + x) mod y == x mod y);
-axiom (forall x: int, y: int :: { (x - y) % y } 0 <= x - y && 0 <= y ==> (x - y) % y == x % y);
+axiom (forall x: int, y: int :: { (x - y) mod y } 0 <= x - y && 0 <= y ==> (x - y) mod y == x mod y);
-axiom (forall a: int, b: int, d: int :: { a % d,b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
+axiom (forall a: int, b: int, d: int :: { a mod d,b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b);
axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i);
@@ -354,7 +354,7 @@ axiom (forall i: int, j: int :: 0 <= j ==> #shl(i, j + 1) == #shl(i, j) * 2); axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i);
-axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) / 2);
+axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) div 2);
const unique $UnknownRef: ref;
diff --git a/Test/test20/Answer b/Test/test20/Answer index efa5bced..fa33507e 100644 --- a/Test/test20/Answer +++ b/Test/test20/Answer @@ -118,7 +118,7 @@ axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3)); const intSet1: Set int;
-axiom (forall x: int :: intSet1[x] == (x == 0 - 5 || x == 3));
+axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3));
procedure P();
@@ -126,7 +126,7 @@ procedure P(); implementation P()
{
- assert (forall x: int :: union(intSet0, intSet1)[x] == (x == 0 - 5 || x == 0 || x == 2 || x == 3));
+ assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3));
}
@@ -143,7 +143,7 @@ axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3); const intSet1: Set int;
-axiom (forall x: int :: intSet1[x] <==> x == 0 - 5 || x == 3);
+axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3);
procedure P();
@@ -151,7 +151,7 @@ procedure P(); implementation P()
{
- assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == 0 - 5 || x == 0 || x == 2 || x == 3);
+ assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3);
}
diff --git a/Test/test20/Prog0.bpl b/Test/test20/Prog0.bpl index ea71b8a8..8fc7b7c7 100644 --- a/Test/test20/Prog0.bpl +++ b/Test/test20/Prog0.bpl @@ -1,5 +1,5 @@ // Let's test some Boogie 2 features ...
-type real;
+
type elements;
type Field a;
diff --git a/Test/test20/Prog1.bpl b/Test/test20/Prog1.bpl index 1d75805c..0e9413c1 100644 --- a/Test/test20/Prog1.bpl +++ b/Test/test20/Prog1.bpl @@ -1,5 +1,5 @@ // Let's test some Boogie 2 features ...
-type real;
+
type elements;
type Field a;
diff --git a/Test/test21/Answer b/Test/test21/Answer index 914e56a1..28aa4e8b 100644 --- a/Test/test21/Answer +++ b/Test/test21/Answer @@ -278,6 +278,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
+--------------------- File Real.bpl ----------------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
@@ -549,6 +552,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
+--------------------- File Real.bpl ----------------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
@@ -826,6 +832,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
+--------------------- File Real.bpl ----------------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl new file mode 100644 index 00000000..3dcf3ea3 --- /dev/null +++ b/Test/test21/Real.bpl @@ -0,0 +1,17 @@ +axiom (forall r: real :: r == 0.0 || r / r == 1.0);
+
+procedure P(a: real, b: real) returns () {
+ assume a >= b && a != 0.0 && a >= 1.3579;
+
+ assert 2e0 * (a + 3.0) - 0.5 >= b;
+ assert 2e0 * (a + 3.0) - 0.5 > b;
+ assert b <= 2e0 * (a + 3.0) - 0.5;
+ assert b < 2e0 * (a + 3.0) - 0.5;
+
+ assert 1/2 <= 0.65;
+ assert a > 100e-2 ==> 1 / a <= a;
+ assert a / 2 != a || a == 0.00;
+ assert a != 0.0 ==> a / a == 1.0;
+
+ assert int(a) >= 0 ==> real(3) * a > a;
+}
\ No newline at end of file diff --git a/Test/test21/runtest.bat b/Test/test21/runtest.bat index d994a4da..bfdcc570 100644 --- a/Test/test21/runtest.bat +++ b/Test/test21/runtest.bat @@ -4,6 +4,7 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
rem set BGEXE=mono ..\..\Binaries\Boogie.exe
+
for %%m in (
n p a
) do (
@@ -16,7 +17,8 @@ for %%f in (DisjointDomains.bpl DisjointDomains2.bpl FunAxioms.bpl Keywords.bpl Casts.bpl BooleanQuantification.bpl EmptyList.bpl Boxing.bpl
MapOutputTypeParams.bpl ParallelAssignment.bpl BooleanQuantification2.bpl
Flattening.bpl Orderings.bpl Orderings2.bpl Orderings3.bpl Orderings4.bpl
- EmptySetBug.bpl Coercions2.bpl MapAxiomsConsistency.bpl LargeLiterals0.bpl) do (
+ EmptySetBug.bpl Coercions2.bpl MapAxiomsConsistency.bpl LargeLiterals0.bpl
+ Real.bpl) do (
echo --------------------- File %%f ----------------------------
%BGEXE% %* /typeEncoding:%%m /logPrefix:0%%m %%f
)
|