summaryrefslogtreecommitdiff
path: root/Test/dafny0/Superposition.dfy
Commit message (Collapse)AuthorAge
* This changeset changes the default visibility of a function/predicate body ↵Gravatar leino2015-03-09
| | | | | | | | | | 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
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* Dafny: improved checking of inherited postconditions (in refinements)Gravatar Unknown2012-09-10