From a9c6c8fcf205a13c759c6f09e69b01d3b144df94 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 28 Sep 2012 15:19:53 -0700 Subject: Dafny: removed div/mod axioms, since Boogie now interprets div/mod Dafny: included FloydCycleDetect again (which had been temporarily commented out) DafnyExtension: adjusted to Boogie's change in abstract-interpretation support --- Binaries/DafnyPrelude.bpl | 15 --------------- 1 file changed, 15 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 53e8e86a..5530f8a7 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -610,18 +610,3 @@ type TickType; var $Tick: TickType; // --------------------------------------------------------------- -// -- Arithmetic ------------------------------------------------- -// --------------------------------------------------------------- - -// the connection between mod and div -axiom (forall x:int, y:int :: {x mod y} {x div y} x mod y == x - x div y * y); - -// remainder is always Euclidean Modulus. -axiom (forall x:int, y:int :: {x mod y} 0 < y ==> 0 <= x mod y && x mod y < y); -axiom (forall x:int, y:int :: {x mod y} y < 0 ==> 0 <= x mod y && x mod y < -y); - -// the following axiom has some unfortunate matching, but it does state a property about mod that -// is sometimes useful -axiom (forall a: int, b: int, d: int :: { a mod d, b mod d } 2 <= d && a mod d == b mod d && a < b ==> a + d <= b); - -// --------------------------------------------------------------- -- cgit v1.2.3