summaryrefslogtreecommitdiff
path: root/Binaries/DafnyRuntime.cs
diff options
context:
space:
mode:
authorGravatar Jason Koenig <unknown>2011-07-08 14:18:37 -0700
committerGravatar Jason Koenig <unknown>2011-07-08 14:18:37 -0700
commit3bfae100a8b18420a26ae460853cc170fd7952f1 (patch)
treebe277b1030bd94c11bd2b2e019c3a06b68374074 /Binaries/DafnyRuntime.cs
parentb620abbcefa269379781d90ce34c538cd7be268e (diff)
Dafny: Dafny now uses the Euclidean definition of division. (Verifier and runtime.)
Diffstat (limited to 'Binaries/DafnyRuntime.cs')
-rw-r--r--Binaries/DafnyRuntime.cs36
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);
+ }
+ }
}
}