diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-27 00:56:15 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-27 00:56:15 -0700 |
| commit | 0de8c9463a1e948fd11d9fe34c729f26b3e1af1b (patch) | |
| tree | 927f94e5ddb259d493551fe0d87d2c134dcd7858 /Test/dafny0/Basics.dfy | |
| parent | 172751103cce5c6615df5613c48ddb5b1ae6fa7a (diff) | |
Dafny: added chaining operators
Diffstat (limited to 'Test/dafny0/Basics.dfy')
| -rw-r--r-- | Test/dafny0/Basics.dfy | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index e6b9a87d..c02f2c45 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -42,3 +42,26 @@ method TestCalls(k: nat) { // assert r == s; // error: G(k) and G(k+k) are different
}
}
+
+// ---------- chaining operators ------------------------------------
+
+function UpTruth(j: int, k: int): bool
+ requires 10 <= j < 180 < 220 <= k;
+{
+ 0 < 2 <= 2 < j != 200 < k < k + 1
+}
+
+function DownTruth(j: int, k: int): bool
+ requires k >= 220 > 180 > j >= 10;
+{
+ k + 1 > k > 200 != j > 2 >= 2 > 0
+}
+
+method ChallengeTruth(j: int, k: int)
+ requires 80 <= j < 150 && 250 <= k < 1000;
+{
+ assert UpTruth(j, k);
+ assert DownTruth(j, k);
+ // but this is not equally true:
+ assert j <= j + k != k + j + 1 < k+k+j <=/*this is the error*/ j+j+k < k+k+j+j == 2*k + 2*j == 2*(k+j);
+}
|