From 9e7c3594b662f1c3102d419104da453d83eddfcd Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 15 Sep 2009 19:04:52 +0000
Subject: 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.

---
 Binaries/DafnyPrelude.bpl | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'Binaries')

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);
 
-- 
cgit v1.2.3