From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/textbook/DivMod.bpl | 130 +++++++++++++++++++++++------------------------ 1 file changed, 65 insertions(+), 65 deletions(-) (limited to 'Test/textbook/DivMod.bpl') diff --git a/Test/textbook/DivMod.bpl b/Test/textbook/DivMod.bpl index bdbc4f19..0af38ec8 100644 --- a/Test/textbook/DivMod.bpl +++ b/Test/textbook/DivMod.bpl @@ -1,65 +1,65 @@ -// RUN: %boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// This file contains two definitions of integer div/mod (truncated division, as is -// used in C, C#, Java, and several other languages, and Euclidean division, which -// has mathematical appeal and is used by SMT Lib) and proves the correct -// correspondence between the two. -// -// Rustan Leino, 23 Sep 2010 - -function abs(x: int): int { if 0 <= x then x else -x } - -function divt(int, int): int; -function modt(int, int): int; - -axiom (forall a,b: int :: divt(a,b)*b + modt(a,b) == a); -axiom (forall a,b: int :: - (0 <= a ==> 0 <= modt(a,b) && modt(a,b) < abs(b)) && - (a < 0 ==> -abs(b) < modt(a,b) && modt(a,b) <= 0)); - -function dive(int, int): int; -function mode(int, int): int; - -axiom (forall a,b: int :: dive(a,b)*b + mode(a,b) == a); -axiom (forall a,b: int :: 0 <= mode(a,b) && mode(a,b) < abs(b)); - -procedure T_from_E(a,b: int) returns (q,r: int) - requires b != 0; - // It would be nice to prove: - // ensures q == divt(a,b); - // ensures r == modt(a,b); - // but since we know that the axioms about divt/modt have unique solutions (for - // non-zero b), we just prove that the axioms hold. - ensures q*b + r == a; - ensures 0 <= a ==> 0 <= r && r < abs(b); - ensures a < 0 ==> -abs(b) < r && r <= 0; -{ - // note, this implementation uses only dive/mode - var qq,rr: int; - qq := dive(a,b); - rr := mode(a,b); - - q := if 0 <= a || rr == 0 then qq else if 0 <= b then qq+1 else qq-1; - r := if 0 <= a || rr == 0 then rr else if 0 <= b then rr-b else rr+b; - assume {:captureState "end of T_from_E"} true; -} - -procedure E_from_T(a,b: int) returns (q,r: int) - requires b != 0; - // It would be nice to prove: - // ensures q == dive(a,b); - // ensures r == mode(a,b); - // but since we know that the axioms about dive/mode have unique solutions (for - // non-zero b), we just prove that the axioms hold. - ensures q*b + r == a; - ensures 0 <= r; - ensures r < abs(b); -{ - // note, this implementation uses only divt/modt - var qq,rr: int; - qq := divt(a,b); - rr := modt(a,b); - - q := if 0 <= rr then qq else if 0 < b then qq-1 else qq+1; - r := if 0 <= rr then rr else if 0 < b then rr+b else rr-b; -} +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// This file contains two definitions of integer div/mod (truncated division, as is +// used in C, C#, Java, and several other languages, and Euclidean division, which +// has mathematical appeal and is used by SMT Lib) and proves the correct +// correspondence between the two. +// +// Rustan Leino, 23 Sep 2010 + +function abs(x: int): int { if 0 <= x then x else -x } + +function divt(int, int): int; +function modt(int, int): int; + +axiom (forall a,b: int :: divt(a,b)*b + modt(a,b) == a); +axiom (forall a,b: int :: + (0 <= a ==> 0 <= modt(a,b) && modt(a,b) < abs(b)) && + (a < 0 ==> -abs(b) < modt(a,b) && modt(a,b) <= 0)); + +function dive(int, int): int; +function mode(int, int): int; + +axiom (forall a,b: int :: dive(a,b)*b + mode(a,b) == a); +axiom (forall a,b: int :: 0 <= mode(a,b) && mode(a,b) < abs(b)); + +procedure T_from_E(a,b: int) returns (q,r: int) + requires b != 0; + // It would be nice to prove: + // ensures q == divt(a,b); + // ensures r == modt(a,b); + // but since we know that the axioms about divt/modt have unique solutions (for + // non-zero b), we just prove that the axioms hold. + ensures q*b + r == a; + ensures 0 <= a ==> 0 <= r && r < abs(b); + ensures a < 0 ==> -abs(b) < r && r <= 0; +{ + // note, this implementation uses only dive/mode + var qq,rr: int; + qq := dive(a,b); + rr := mode(a,b); + + q := if 0 <= a || rr == 0 then qq else if 0 <= b then qq+1 else qq-1; + r := if 0 <= a || rr == 0 then rr else if 0 <= b then rr-b else rr+b; + assume {:captureState "end of T_from_E"} true; +} + +procedure E_from_T(a,b: int) returns (q,r: int) + requires b != 0; + // It would be nice to prove: + // ensures q == dive(a,b); + // ensures r == mode(a,b); + // but since we know that the axioms about dive/mode have unique solutions (for + // non-zero b), we just prove that the axioms hold. + ensures q*b + r == a; + ensures 0 <= r; + ensures r < abs(b); +{ + // note, this implementation uses only divt/modt + var qq,rr: int; + qq := divt(a,b); + rr := modt(a,b); + + q := if 0 <= rr then qq else if 0 < b then qq-1 else qq+1; + r := if 0 <= rr then rr else if 0 < b then rr+b else rr-b; +} -- cgit v1.2.3