diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | db6ef6c9e2bca859280cfbe17871c38da74977fc (patch) | |
| tree | d742312e6c9c69386f4c7111d9133ccc3d810e01 /Test/dafny0/Simple.dfy | |
Initial set of files.
Diffstat (limited to 'Test/dafny0/Simple.dfy')
| -rw-r--r-- | Test/dafny0/Simple.dfy | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy new file mode 100644 index 00000000..9f89543c --- /dev/null +++ b/Test/dafny0/Simple.dfy @@ -0,0 +1,29 @@ +// My first Dafny program
+// Rustan Leino, 27 January 2008
+
+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;
+ }
+ call t, u, v := M(true, lotsaObjects);
+ var to: MyClass<T,U>;
+ call to, u, v := this.M(true, lotsaObjects);
+ call to, u, v := to.M(true, lotsaObjects);
+ }
+ }
+}
|