summaryrefslogtreecommitdiff
path: root/Test/dafny1
diff options
context:
space:
mode:
authorGravatar Aleksandar Milicevic <unknown>2011-08-10 16:38:26 -0700
committerGravatar Aleksandar Milicevic <unknown>2011-08-10 16:38:26 -0700
commit3e63acac9cf380ac6f9e34bd5bf5093f7f581068 (patch)
treeba73ea55af06acd59d7bb1b40f09482b14df8026 /Test/dafny1
parentb95f6aa1be913fe996848a64ad53e63b4f49d4ab (diff)
Jennisys: started to work on synthesizing some methods. So far, only
infrastructural things have been implemented, like handling return parameters, generating different "fresh" spec for methods than for constructors, adding "Valid()" to method preconditions.
Diffstat (limited to 'Test/dafny1')
-rw-r--r--Test/dafny1/ListContents.dfy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy
index f672950b..069ffbde 100644
--- a/Test/dafny1/ListContents.dfy
+++ b/Test/dafny1/ListContents.dfy
@@ -48,7 +48,7 @@ class Node<T> {
r.footprint := {r} + this.footprint;
r.list := [r.data] + this.list;
}
-
+
method ReverseInPlace() returns (reverse: Node<T>)
requires Valid();
modifies footprint;