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.

3 files changed, 25 insertions, 3 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/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 1cac78af..64401071 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/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();

diff --git a/Util/Emacs/chalice-mode.el b/Util/Emacs/chalice-mode.el
index 7a6b6d4c..dc3d469c 100644
--- a/Util/Emacs/chalice-mode.el
+++ b/Util/Emacs/chalice-mode.el
@@ -38,8 +38,8 @@
         "above" "acc" "acquire" "and" "assert" "assigned" "assume"

         "below" "between" "call" "credit"

         "downgrade" "else" "eval" "exists" "fold" "forall" "fork" "free" "havoc" "holds"

-        "if" "in" "install" "ite" "join" "lock" "lockbottom" "maxlock" "module" "new" "nil"

-        "old" "rd" "receive" "release" "result" "send" "share"

+        "if" "in" "ite" "join" "lock" "lockbottom" "maxlock" "module" "new" "nil"

+        "old" "rd" "receive" "release" "reorder" "result" "send" "share"

         "this" "unfold" "unfolding" "unshare" "while"

         "false" "true" "null")) . font-lock-keyword-face)

    `(,(chalice-regexp-opt '("bool" "int" "seq" "token")) . font-lock-type-face)