diff options
| author |  Jason Koenig <unknown> | 2011-07-08 14:18:37 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-08 14:18:37 -0700 |
| commit | 3bfae100a8b18420a26ae460853cc170fd7952f1 (patch) | |
| tree | be277b1030bd94c11bd2b2e019c3a06b68374074 /Binaries | |
| parent | b620abbcefa269379781d90ce34c538cd7be268e (diff) | |
Dafny: Dafny now uses the Euclidean definition of division. (Verifier and runtime.)
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 6 | ||||
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 36 |
2 files changed, 39 insertions, 3 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 94a8833a..dc152185 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -373,12 +373,12 @@ var $Tick: TickType; // the connection between % and /
axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y);
-// sign of denominator determines sign of remainder
+// remainder is always Euclidean Modulus.
axiom (forall x:int, y:int :: {x % y} 0 < y ==> 0 <= x % y && x % y < y);
-axiom (forall x:int, y:int :: {x % y} y < 0 ==> y < x % y && x % y <= 0);
+axiom (forall x:int, y:int :: {x % y} y < 0 ==> 0 <= x % y && x % y < -y);
// the following axiom has some unfortunate matching, but it does state a property about % that
-// is sometime useful
+// is sometimes useful
axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
// ---------------------------------------------------------------
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 46a3f3df..c03ac643 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -267,5 +267,41 @@ namespace Dafny yield return true;
}
}
+ // pre: b != 0
+ // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
+ if (0 <= a.Sign) {
+ if (0 <= b.Sign) {
+ // +a +b: a/b
+ return BigInteger.Divide(a, b);
+ } else {
+ // +a -b: -(a/(-b))
+ return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
+ }
+ } else {
+ if (0 <= b.Sign) {
+ // -a +b: -((-a-1)/b) - 1
+ return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
+ } else {
+ // -a -b: ((-a-1)/(-b)) + 1
+ return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
+ }
+ }
+ }
+ // pre: b != 0
+ // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
+ public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
+ var bp = BigInteger.Abs(b);
+ if (0 <= a.Sign) {
+ // +a: a % b'
+ return BigInteger.Remainder(a, bp);
+ } else {
+ // c = ((-a) % b')
+ // -a: b' - c if c > 0
+ // -a: 0 if c == 0
+ var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
+ return c.IsZero ? c : BigInteger.Subtract(bp, c);
+ }
+ }
}
}
|