From f14dcef0d8c0459638c81f7a82972055cfd5d4f7 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 24 Sep 2010 01:11:16 +0000
Subject: Boogie: * Added Test/textbook/DivMod.bpl, which embodies a conversion
 between C's div/mod operators and SMT Lib's div/mod operators. * Added a
 rudimentary printing of variables for captured states.  It doesn't attempt to
 print everything at this time, and it doesn't work when variables get
 unique-ified by @@-suffixes.  A more complete implementation will be added at
 a later time.

---
 Test/textbook/Answer      |  4 +++
 Test/textbook/DivMod.bpl  | 63 +++++++++++++++++++++++++++++++++++++++++++++++
 Test/textbook/runtest.bat |  2 +-
 3 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 Test/textbook/DivMod.bpl

(limited to 'Test/textbook')

diff --git a/Test/textbook/Answer b/Test/textbook/Answer
index 9e2227dc..538109f5 100644
--- a/Test/textbook/Answer
+++ b/Test/textbook/Answer
@@ -10,3 +10,7 @@ Boogie program verifier finished with 1 verified, 0 errors
 ------------------------------ Bubble.bpl ---------------------
 
 Boogie program verifier finished with 1 verified, 0 errors
+
+------------------------------ DivMod.bpl ---------------------
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/textbook/DivMod.bpl b/Test/textbook/DivMod.bpl
new file mode 100644
index 00000000..4a551b6e
--- /dev/null
+++ b/Test/textbook/DivMod.bpl
@@ -0,0 +1,63 @@
+// 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;
+}
diff --git a/Test/textbook/runtest.bat b/Test/textbook/runtest.bat
index 6e39e589..bdfdd7d5 100644
--- a/Test/textbook/runtest.bat
+++ b/Test/textbook/runtest.bat
@@ -6,7 +6,7 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe
 REM ======================
 REM ====================== Examples written in Boogie
 REM ======================
-for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl) do (
+for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl DivMod.bpl) do (
   echo.
   echo ------------------------------ %%f ---------------------
   %BPLEXE% %* %%f
-- 
cgit v1.2.3