diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-12-30 20:39:58 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-12-30 20:39:58 -0800 |
| commit | 8678d4ddf2d9558e286f1ab3c721ed866e2236f7 (patch) | |
| tree | f35a25fd92df8516fb2e1eb26942cf0981b57970 /Test/generalizedarray | |
| parent | 6344c5f8f46f03e307b27ccb4e60cc2709413ebc (diff) | |
added a test for generalized array theory
Diffstat (limited to 'Test/generalizedarray')
| -rw-r--r-- | Test/generalizedarray/Answer | 4 | ||||
| -rw-r--r-- | Test/generalizedarray/Maps.bpl | 59 | ||||
| -rw-r--r-- | Test/generalizedarray/runtest.bat | 12 |
3 files changed, 75 insertions, 0 deletions
diff --git a/Test/generalizedarray/Answer b/Test/generalizedarray/Answer new file mode 100644 index 00000000..285316aa --- /dev/null +++ b/Test/generalizedarray/Answer @@ -0,0 +1,4 @@ +
+-------------------- Maps.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/generalizedarray/Maps.bpl b/Test/generalizedarray/Maps.bpl new file mode 100644 index 00000000..69aa86b0 --- /dev/null +++ b/Test/generalizedarray/Maps.bpl @@ -0,0 +1,59 @@ +type X;
+
+function {:builtin "MapAdd"} mapadd([X]int, [X]int) : [X]int;
+function {:builtin "MapSub"} mapsub([X]int, [X]int) : [X]int;
+function {:builtin "MapMul"} mapmul([X]int, [X]int) : [X]int;
+function {:builtin "MapDiv"} mapdiv([X]int, [X]int) : [X]int;
+function {:builtin "MapMod"} mapmod([X]int, [X]int) : [X]int;
+function {:builtin "MapConst"} mapconstint(int) : [X]int;
+function {:builtin "MapConst"} mapconstbool(bool) : [X]bool;
+function {:builtin "MapAnd"} mapand([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapOr"} mapor([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapNot"} mapnot([X]bool) : [X]bool;
+function {:builtin "MapIte"} mapiteint([X]bool, [X]int, [X]int) : [X]int;
+function {:builtin "MapIte"} mapitebool([X]bool, [X]bool, [X]bool) : [X]bool;
+function {:builtin "MapLe"} maple([X]int, [X]int) : [X]bool;
+function {:builtin "MapLt"} maplt([X]int, [X]int) : [X]bool;
+function {:builtin "MapGe"} mapge([X]int, [X]int) : [X]bool;
+function {:builtin "MapGt"} mapgt([X]int, [X]int) : [X]bool;
+function {:builtin "MapEq"} mapeq([X]int, [X]int) : [X]bool;
+function {:builtin "MapIff"} mapiff([X]bool, [X]bool) : [X]bool;
+function {:builtin "MapImp"} mapimp([X]bool, [X]bool) : [X]bool;
+
+
+
+const FF: [X]bool;
+axiom FF == mapconstbool(false);
+
+const TT: [X]bool;
+axiom TT == mapconstbool(true);
+
+const MultisetEmpty: [X]int;
+axiom MultisetEmpty == mapconstint(0);
+
+function {:inline} MultisetSingleton(x: X) : [X]int
+{
+ MultisetEmpty[x := 1]
+}
+
+function {:inline} MultisetPlus(a: [X]int, b: [X]int) : [X]int
+{
+ mapadd(a, b)
+}
+
+function {:inline} MultisetMinus(a: [X]int, b: [X]int) : [X]int
+{
+ mapiteint(mapgt(a, b), mapsub(a, b), mapconstint(0))
+}
+
+procedure foo() {
+ var x: X;
+
+ assert FF != TT;
+ assert mapnot(FF) == TT;
+
+ assert MultisetSingleton(x) != MultisetEmpty;
+ assert MultisetPlus(MultisetEmpty, MultisetSingleton(x)) == MultisetSingleton(x);
+ assert MultisetMinus(MultisetPlus(MultisetEmpty, MultisetSingleton(x)), MultisetSingleton(x)) == MultisetEmpty;
+ assert MultisetMinus(MultisetEmpty, MultisetSingleton(x)) == MultisetEmpty;
+}
\ No newline at end of file diff --git a/Test/generalizedarray/runtest.bat b/Test/generalizedarray/runtest.bat new file mode 100644 index 00000000..1f4c64f9 --- /dev/null +++ b/Test/generalizedarray/runtest.bat @@ -0,0 +1,12 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (Maps.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BPLEXE% %* /typeEncoding:m /useArrayTheory %%f
+)
+
|