diff options
author | leino <unknown> | 2015-03-09 10:12:44 -0700 |
---|---|---|
committer | leino <unknown> | 2015-03-09 10:12:44 -0700 |
commit | efeb1c5ddde488b4923d87339b8ebbf75d910e16 (patch) | |
tree | dc44c9b431f1f24889047b736d8720c2a89d794e /Test/dafny2 | |
parent | 1157b689cbc7c65cde1f20192e8b3b49046d6fc4 (diff) |
This changeset changes the default visibility of a function/predicate body outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'.
Semantics of 'protected':
* The definition (i.e., body) of a 'protected' function is not visible outside the defining module
* The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions.
* In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected'
* The 'protected' status of a function must be preserved in refinement modules
Diffstat (limited to 'Test/dafny2')
-rw-r--r-- | Test/dafny2/MonotonicHeapstate.dfy | 6 | ||||
-rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/Test/dafny2/MonotonicHeapstate.dfy b/Test/dafny2/MonotonicHeapstate.dfy index d6817ce9..b0032b44 100644 --- a/Test/dafny2/MonotonicHeapstate.dfy +++ b/Test/dafny2/MonotonicHeapstate.dfy @@ -12,7 +12,7 @@ module M0 { ghost var Repr: set<object>;
- predicate Valid()
+ protected predicate Valid()
reads this, Repr;
{
this in Repr && null !in Repr &&
@@ -58,7 +58,7 @@ module M1 refines M0 { class Expr {
ghost var resolved: bool;
- predicate Valid()
+ protected predicate Valid()
{
resolved ==>
(kind == Binary ==> left.resolved && right.resolved)
@@ -104,7 +104,7 @@ module M2 refines M1 { class Expr {
var decl: VarDecl; // if kind==Ident, filled in during resolution
- predicate Valid()
+ protected predicate Valid()
{
resolved ==>
(kind == Ident ==> decl != null)
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
}
|