diff options
| author |  Jason Koenig <unknown> | 2011-07-08 14:50:26 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-08 14:50:26 -0700 |
| commit | 32bd4d4b3b892d0bbace511372ca53dd8ffad63c (patch) | |
| tree | c1bc60a02940de7e3b8a0f71a56af0e0369c7a06 /Test/dafny0/Basics.dfy | |
| parent | 2955170d9183a7bb8598ce89a61818623f321f16 (diff) | |
Dafny: Added Euclidean regression test (Verifier only).
Diffstat (limited to 'Test/dafny0/Basics.dfy')
| -rw-r--r-- | Test/dafny0/Basics.dfy | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index 1ae5b9c4..6aa1e34d 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -171,3 +171,17 @@ method SwapEm(a: int, b: int) returns (x: int, y: int) {
x, y := b, a;
}
+
+function method abs(a:int): int
+{
+ if a <= 0 then -a else a
+}
+// test of verifier using euclidean division.
+method EuclideanTest(a: int, b: int)
+ requires b != 0;
+{
+ var q, r := a / b, a % b;
+ assert 0 <= r < abs(b);
+ assert a == b * q + r;
+ assert (a/b) * b + a % b == a;
+}
\ No newline at end of file |