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 | 83e13f515b7d9f89a96c670d34b9576b61edb894 (patch) | |
| tree | 2ac714bc509cf9940fc96cd8830222c16097864a /Test/dafny0/PredExpr.dfy | |
| parent | d9bdc81cd145329fadacc779255e0faf4b935bd5 (diff) | |
Dafny: added assert/assume expressions
Diffstat (limited to 'Test/dafny0/PredExpr.dfy')
| -rw-r--r-- | Test/dafny0/PredExpr.dfy | 43 |
1 files changed, 43 insertions, 0 deletions
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;
+}
|