summaryrefslogtreecommitdiff
path: root/Test/dafny2/StoreAndRetrieve.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny2/StoreAndRetrieve.dfy')
-rw-r--r--Test/dafny2/StoreAndRetrieve.dfy4
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index e39913a8..5314b6fa 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -5,7 +5,7 @@ abstract module A {
import L = Library
class {:autocontracts} StoreAndRetrieve<Thing(==)> {
ghost var Contents: set<Thing>;
- predicate Valid()
+ protected predicate Valid()
{
true
}
@@ -31,7 +31,7 @@ abstract module A {
module B refines A {
class StoreAndRetrieve<Thing(==)> {
var arr: seq<Thing>;
- predicate Valid()
+ protected predicate Valid()
{
Contents == set x | x in arr
}