summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-09-30 16:36:23 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-09-30 16:36:23 -0700
commit118cb0f58e5468b0801d2483875662831b8a82d6 (patch)
treebcd08d3b276442cdfd4d60d20e4101dc737c6d47 /Test
parentad80221cf26f0a75c534548d6483c3f963b742cd (diff)
Dafny: Updated snapshotable tree to remove IsReadonly precondition for CreateIterator.
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny2/SnapshotableTrees.dfy20
1 files changed, 19 insertions, 1 deletions
diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy
index 0c31d8f3..3386b123 100644
--- a/Test/dafny2/SnapshotableTrees.dfy
+++ b/Test/dafny2/SnapshotableTrees.dfy
@@ -147,7 +147,7 @@ class Tree
}
method CreateIterator() returns (iter: Iterator)
- requires Valid() && IsReadonly;
+ requires Valid(); // && IsReadonly;
ensures iter != null && iter.Valid() && fresh(iter.IterRepr);
ensures iter.T == this && iter.Contents == Contents && iter.N == -1;
{
@@ -459,3 +459,21 @@ class Iterator
}
datatype List = Nil | Cons(Node, List);
+
+/* The following method shows the problem of concurrent modifications and shows that the
+ * design of the snapshotable trees herein handle this correctly. That is, after inserting
+ * into a tree that is being iterated, use of the associated iterator can no longer be
+ * proved to be correct.
+ *
+method TestConcurrentModification(t: Tree)
+ requires t != null && t.Valid() && !t.IsReadonly;
+ modifies t.MutableRepr;
+{
+ var it := t.CreateIterator();
+ var more := it.MoveNext();
+ if (more) {
+ var pos := t.Insert(52); // this modification of the collection renders all associated iterators invalid
+ more := it.MoveNext(); // error: operation t.Insert may have made this iterator invalid
+ }
+}
+*/