diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-11-09 17:27:36 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-11-09 17:27:36 -0800 |
| commit | cea05485e8f58b1831bc5a1c68178164927f1c5b (patch) | |
| tree | 5487b3c5829be18581a7978b80efa537b444e782 /Test/dafny0 | |
| parent | 29524a38ed773a399011f42526c80ed790ce83d6 (diff) | |
Dafny: added assert/assume expressions
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 11 | ||||
| -rw-r--r-- | Test/dafny0/PredExpr.dfy | 43 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
3 files changed, 55 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index bae3aa50..bcdb7126 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1311,3 +1311,14 @@ CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost -------------------- MultiSets.dfy --------------------
Dafny program verifier finished with 22 verified, 0 errors
+
+-------------------- PredExpr.dfy --------------------
+PredExpr.dfy(23,15): Error: value assigned to a nat must be non-negative
+Execution trace:
+ (0,0): anon6_Else
+ (0,0): anon7_Else
+PredExpr.dfy(36,17): Error: condition in assert expression might not hold
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 7 verified, 2 errors
diff --git a/Test/dafny0/PredExpr.dfy b/Test/dafny0/PredExpr.dfy new file mode 100644 index 00000000..3499a01c --- /dev/null +++ b/Test/dafny0/PredExpr.dfy @@ -0,0 +1,43 @@ +function Subonacci(n: nat): nat
+{
+ if 2 <= n then
+ // proving that this case is a nat requires more information,
+ // which is here supplied by an assume expression
+ assume Subonacci(n-2) <= Subonacci(n-1);
+ Subonacci(n-1) - Subonacci(n-2)
+ else
+ n
+}
+
+function F(n: int): nat
+{
+ Subonacci(assume 0 <= n; n) -
+ Subonacci(n)
+}
+
+function G(n: int, b: bool): nat
+{
+ if b then
+ Subonacci(assume 0 <= n; n)
+ else
+ Subonacci(n) // error: n may not be a nat
+}
+
+ghost method M(m: nat, n: int)
+{
+ var k := F(m);
+ assert k == 0;
+ k := F(n);
+ assert k == 0; // this is still known
+}
+
+method M0(j: int) returns (n: nat)
+{
+ n := assert 0 <= j; j; // error: j may be negative
+}
+
+method M1(j: int) returns (n: nat)
+{
+ n := (assume 0 <= j; j) + (assert 0 <= j; j);
+ assert n == 2*j;
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index c30ec3a5..32a60340 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -20,7 +20,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
Refinement.dfy RefinementErrors.dfy LoopModifies.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
- CallStmtTests.dfy MultiSets.dfy) do (
+ CallStmtTests.dfy MultiSets.dfy PredExpr.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
|