diff options
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 6 |
1 files changed, 3 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);
// ---------------------------------------------------------------
|