| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | This changeset changes the default visibility of a function/predicate body ↵ |  leino | 2015-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 | ||
| * | Stop pretty-print from emitting deprecated semi-colons. | qunyanm | 2015-03-05 |
| | | |||
| * | Disallow parentheses-less declarations of predicates and co-predicates, ↵ | leino | 2014-08-27 |
| | | | | | along with a backward-compatibility warning message if such declarations are attempted | ||
| * | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
| | | |||
| * | Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, ↵ | Rustan Leino | 2013-04-01 |
| | | | | | | | | where more type information is known Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement. Fixed numerous places where some recursive checks did not reach. | ||
| * | renamed "abstract module" to "module facade" |  Rustan Leino | 2012-10-22 |
| | | | | | renamed "ghost module" to "abstract module", adding a keyword "abstract" | ||
| * | improved and fixed compilation and resolution of assign-such-that statements | Rustan Leino | 2012-10-05 |
| | | |||
| * | Dafny: updated test suite to new syntax | Jason Koenig | 2012-07-30 |
| | | |||
| * | Dafny: restored soundness for refinement by disallowing certain updates and ↵ | Jason Koenig | 2012-07-11 |
| | | | | | method calls | ||
| * | Dafny: reinstated autocontracts | Jason Koenig | 2012-07-02 |
| | | |||
| * | Dafny: fixed a couple of compiler bugs |  Unknown | 2012-06-14 |
| | | |||
| * | Dafny: support assign-such-that in var declarations in refinements | Unknown | 2012-03-15 |
| | | |||
| * | Dafny: added StoreAndRetrieve refinement example | Unknown | 2012-03-15 |
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |