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/DafnyRuntime.cs | |
| parent | b620abbcefa269379781d90ce34c538cd7be268e (diff) | |
Dafny: Dafny now uses the Euclidean definition of division. (Verifier and runtime.)
Diffstat (limited to 'Binaries/DafnyRuntime.cs')
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 36 |
1 files changed, 36 insertions, 0 deletions
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);
+ }
+ }
}
}
|