Dafny: Added axioms for division and modulo.

Dafny:  Make use of function preconditions in function well-definedness checks.
Chalice:  Changed old "install" to current "reorder" keyword in Emacs mode.

2 files changed, 23 insertions, 1 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 9ff60f1b..40928306 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -189,6 +189,19 @@ axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }
 

 // ---------------------------------------------------------------

 

+// 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

+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);

+

+// the following axiom has some unfortunate matching, but it does state a property about % that

+// is sometime useful

+axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b  ==>  a + d <= b);

+

+// ---------------------------------------------------------------

+

 type $token;

 function $file_name_is(id:int, tok:$token) returns(bool);

 

diff --git a/Dafny/Translator.ssc b/Dafny/Translator.ssc
index 1cac78af..64401071 100644
--- a/Dafny/Translator.ssc
+++ b/Dafny/Translator.ssc
@@ -589,6 +589,7 @@ namespace Microsoft.Dafny {
       requires f.Body != null;

     {

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);

+      // parameters of the procedure

       Bpl.VariableSeq inParams = new Bpl.VariableSeq();

       Bpl.Expr wh = Bpl.Expr.And(

         Bpl.Expr.Neq(new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), predef.Null),

@@ -601,8 +602,16 @@ namespace Microsoft.Dafny {
         inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, varType, wh), true));

       }

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

+      // preconditions of the procedure

+      Bpl.RequiresSeq req = new Bpl.RequiresSeq();

+      string comment = "user-defined preconditions";

+      foreach (Expression p in f.Req) {

+        req.Add(Requires(p.tok, false, etran.TrExpr(p), null, comment));

+        comment = null;

+      }

+      // the procedure itself

       Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),

-        new Bpl.RequiresSeq(), new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());

+        req, new Bpl.IdentifierExprSeq(), new Bpl.EnsuresSeq());

       sink.TopLevelDeclarations.Add(proc);

 

       Bpl.VariableSeq localVariables = new Bpl.VariableSeq();