diff options
| author |  wuestholz <unknown> | 2014-05-29 21:41:00 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-05-29 21:41:00 +0200 |
| commit | 607ef28aadb281ab61a2be493a637126e967a388 (patch) | |
| tree | aae16c049c860e443920f9c6ee31af4e35f8a800 /Test/dafny0/Simple.dfy.expect | |
| parent | dc0a9130355352d0f47e07232d8119fc7219ccbc (diff) | |
Set up the same test infrastructure as in Boogie.
Diffstat (limited to 'Test/dafny0/Simple.dfy.expect')
| -rw-r--r-- | Test/dafny0/Simple.dfy.expect | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/Test/dafny0/Simple.dfy.expect b/Test/dafny0/Simple.dfy.expect new file mode 100644 index 00000000..c187ffe1 --- /dev/null +++ b/Test/dafny0/Simple.dfy.expect @@ -0,0 +1,66 @@ +// c:\codeplex\dafny\Test\dafny0\Simple.dfy
+
+class MyClass<T, U> {
+ var x: int;
+
+ method M(s: bool, lotsaObjects: set<object>)
+ returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)
+ requires s;
+ modifies this, lotsaObjects;
+ ensures t == t;
+ ensures old(null) != this;
+ {
+ x := 12;
+ while x < 100
+ invariant x <= 100;
+ {
+ x := x + 17;
+ if x % 20 == 3 {
+ x := this.x + 1;
+ } else {
+ this.x := x + 0;
+ }
+ t, u, v := M(true, lotsaObjects);
+ var to: MyClass<T,U>;
+ to, u, v := this.M(true, lotsaObjects);
+ to, u, v := to.M(true, lotsaObjects);
+ assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
+ }
+ }
+
+ function F(x: int, y: int, h: WildData, k: WildData): WildData
+ {
+ if x < 0 then
+ h
+ else if x == 0 then
+ if if h == k then true else false then
+ h
+ else if y == 0 then
+ k
+ else
+ h
+ else
+ k
+ }
+}
+
+datatype List<T> = Nil | Cons(T, List<T>)
+
+datatype WildData = Something | JustAboutAnything(bool, myName: set<int>, int, WildData) | More(List<int>)
+
+class C {
+ var w: WildData;
+ var list: List<bool>;
+}
+
+lemma M(x: int)
+ ensures x < 8;
+{
+}
+
+colemma M'(x': int)
+ ensures true;
+{
+}
+
+Dafny program verifier finished with 0 verified, 0 errors
|