Dafny: Dafny now uses the Euclidean definition of division. (Verifier and runtime.)

2 files changed, 15 insertions, 6 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/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 920105a9..d61d653d 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -1375,10 +1375,19 @@ namespace Microsoft.Dafny {
           case BinaryExpr.ResolvedOpcode.Mul:

             opString = "*";  break;

           case BinaryExpr.ResolvedOpcode.Div:

-            opString = "/";  break;

+            wr.Write("Dafny.Helpers.EuclideanDivision(");

+            TrParenExpr(e.E0);

+            wr.Write(", ");

+            TrExpr(e.E1);

+            wr.Write(")");

+            break;

           case BinaryExpr.ResolvedOpcode.Mod:

-            opString = "%";  break;

-

+            wr.Write("Dafny.Helpers.EuclideanModulus(");

+            TrParenExpr(e.E0);

+            wr.Write(", ");

+            TrExpr(e.E1);

+            wr.Write(")");

+            break;

           case BinaryExpr.ResolvedOpcode.SetEq:

           case BinaryExpr.ResolvedOpcode.SeqEq:

             callString = "Equals";  break;