diff options
| author |  rustanleino <unknown> | 2010-09-24 01:11:16 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-09-24 01:11:16 +0000 |
| commit | f14dcef0d8c0459638c81f7a82972055cfd5d4f7 (patch) | |
| tree | 28295afd3933d73e79d527b4381cb36679ca82a2 /Test/textbook | |
| parent | a04d88a901acc617b5270c8553f4680916ca216f (diff) | |
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.
Diffstat (limited to 'Test/textbook')
| -rw-r--r-- | Test/textbook/Answer | 4 | ||||
| -rw-r--r-- | Test/textbook/DivMod.bpl | 63 | ||||
| -rw-r--r-- | Test/textbook/runtest.bat | 2 |
3 files changed, 68 insertions, 1 deletions
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
|