diff options
| author |  Rustan Leino <unknown> | 2013-08-06 03:52:25 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-06 03:52:25 -0700 |
| commit | dd65717941251e2be9df829694a42ec4d015bb53 (patch) | |
| tree | 87a044a7a8a16d569aa3bb969df08c367b14ed73 /Test/dafny0/StatementExpressions.dfy | |
| parent | 739d4aeff0124e69e30f17880d403b59fd008670 (diff) | |
Allow calls to side-effect-free ghost methods from expressions
Diffstat (limited to 'Test/dafny0/StatementExpressions.dfy')
| -rw-r--r-- | Test/dafny0/StatementExpressions.dfy | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/Test/dafny0/StatementExpressions.dfy b/Test/dafny0/StatementExpressions.dfy index 9f33b282..386d030b 100644 --- a/Test/dafny0/StatementExpressions.dfy +++ b/Test/dafny0/StatementExpressions.dfy @@ -56,3 +56,32 @@ ghost method Q(n: nat) assert y == 102; // error: assertion does not hold
}
}
+
+// ---------------------
+
+function Fact(n: nat): nat
+{
+ if n == 0 then 1 else n * Fact(n-1)
+}
+
+lemma L(n: nat)
+ ensures 1 <= Fact(n);
+{
+}
+
+function F_Fails(n: nat): int
+{
+ 50 / Fact(n) // error: possible division by zero
+}
+
+function F_Succeeds(n: nat): int
+{
+ L(n);
+ 50 / Fact(n)
+}
+
+function F_PreconditionViolation(n: int): int
+{
+ L(n); // error: argument might be negative
+ 50 / Fact(n)
+}
|