diff options
Diffstat (limited to 'Test/z3api/boog10.bpl')
-rw-r--r-- | Test/z3api/boog10.bpl | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/Test/z3api/boog10.bpl b/Test/z3api/boog10.bpl index 075432d7..628d275f 100644 --- a/Test/z3api/boog10.bpl +++ b/Test/z3api/boog10.bpl @@ -1,24 +1,24 @@ -type ref;
-// types
-type Color;
-const unique red: Color;
-const unique blue: Color;
-const unique green: Color;
-
-axiom (forall ce:Color :: ce==red || ce==blue || ce==green);
-var myColor: Color;
-
-// procedure
-procedure SetTo(c: Color);
- modifies myColor
-;
-
- ensures myColor==c;
-
-implementation SetTo(c: Color) {
- assert (blue==green);
- myColor:=blue;
-}
-
-
-
+type ref; +// types +type Color; +const unique red: Color; +const unique blue: Color; +const unique green: Color; + +axiom (forall ce:Color :: ce==red || ce==blue || ce==green); +var myColor: Color; + +// procedure +procedure SetTo(c: Color); + modifies myColor +; + + ensures myColor==c; + +implementation SetTo(c: Color) { + assert (blue==green); + myColor:=blue; +} + + + |