diff options
Diffstat (limited to 'Test/dafny2')
-rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy index 93bf1812..1cc906f3 100644 --- a/Test/dafny2/StoreAndRetrieve.dfy +++ b/Test/dafny2/StoreAndRetrieve.dfy @@ -1,6 +1,6 @@ abstract module A {
import L = Library;
- class {:autocontracts} StoreAndRetrieve<Thing> {
+ class {:autocontracts} StoreAndRetrieve<Thing(==)> {
ghost var Contents: set<Thing>;
predicate Valid
{
@@ -26,7 +26,7 @@ abstract module A { }
module B refines A {
- class StoreAndRetrieve<Thing> {
+ class StoreAndRetrieve<Thing(==)> {
var arr: seq<Thing>;
predicate Valid
{
@@ -52,14 +52,14 @@ module B refines A { }
var k := arr[i];
...;
- var a :| assume Contents == set x | x in a;
+ var a: seq<Thing> :| assume Contents == set x | x in a;
arr := a;
}
}
}
module C refines B {
- class StoreAndRetrieve<Thing> {
+ class StoreAndRetrieve<Thing(==)> {
method Retrieve...
{
...;
|