| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
are inherited
from the overridden method and Code Contracts will copy those preconditions to make sure
the right run-time checking happens; when Code Contracts finds preconditions on overrides,
it emits warnings).
|
| |
|
|
| |
trying to substitute the nested CasePattern with the BoundVar.
|
| |\ |
|
| | | |
|
| |/
|
|
| |
the auto-triggers can be computed for ForallStmt.
|
| |
|
|
|
| |
The old syntax, D[f := E], is still supported for a short while, but generates a warning about that syntax being deprecated.
The new syntax also supports multiple updates: D.(f := E0, g := E1, h := E2)
|
| |
|
|
| |
of "if" statements.
|
| |
|
|
| |
This fixes a bug that affected Monad.dfy
|
| |
|
|
|
|
| |
Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and
old(f(x)). This has a number of implications; see the new tests files for more
information.
|
| | |
|
| |\
| |
| |
| |
| | |
Changes that were needed included preventing the InductionRewriter from
iterating on a SplitQuantifier and using the new error reporting engine.
|
| | |
| |
| |
| |
| | |
In particular, start detecting loops between terms that don't look like each
other at the Dafny level, such as {a[x]} and {x in a} (when a is a multiset)
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This requires rewriting the parts of the AST that contain these quantifiers. We
unfortunately don't have facilities to do such rewrites at the moment (and there
are loops in the AST, so it would be hard to write such a facility). As a
workaround, this commit introduces a field in quantifier expressions,
SplitQuantifiers. Code that manipulate triggers is expected to look for this
field, and ignore the other fields if that one is found.
|
| | | |
|
| | |
| |
| |
| | |
This new version will include a cleaner pipeline, and trigger splitting.
|
| | |
| |
| |
| |
| | |
The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.
|
| | |
| |
| |
| |
| |
| | |
clues about which parameters to include.
As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others.
|
| | | |
|
| | | |
|
| |/
|
|
|
| |
Generate warnings for malformed :induction arguments.
Removed the functionality that allowed induction on 'this'.
|
| | |
|
| |\
| |
| |
| |
| | |
This contains trigger related things under the autoTriggers flag (disabled by
default), and some bug-fixes and cleanups that are already enabled.
|
| | | |
|
| | |
| |
| |
| | |
Use an extension method to properly deal with null attributes
|
| |/
|
|
|
| |
BoundVars that are combined in rewriting of the nested match patterns so they
show up in the IDE correctly.
|
| | |
|
| |
|
|
| |
explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
function last<T>(xs: List<T>): T
requires xs != Nil
{
match xs
case Cons(y, Nil) => y
case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
}
And
function minus(x: Nat, y: Nat): Nat
{
match (x, y)
case (Zero, _) => Zero
case (Suc(_), Zero) => x
case (Suc(a), Suc(b)) => minus(a, b)
}
|
| |
|
|
| |
fn in fixupRevealLemma substitute the types as well.
|
| |
|
|
| |
from included files
|
| |
|
|
|
|
| |
F's corresponding F_FULL, make sure the function is indeed the FullVesion
before the substitution. Also keep the TypeArgsSubst for the enclosingClass in
the typeMap.
|
| |
|
|
|
|
|
|
|
|
| |
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
|
| | |
|
| |
|
|
|
|
|
| |
so use the new name resolution machinery that handles modules and type parameters
Included some inadvertently left-out test cases in dafny0/Modules0.dfy
Fixed comparable-types tests
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
class are now
automatically static, and fields are no longer allowed to be declared there. Stated
differently, all heap state must now be declared inside an explicitly declared class,
and functions and methods declared outside any class can be viewed as belonging to
the module. The motivating benefit of this change is to no longer need the 'static'
keyword when declaring a module of functions and methods.
|
| |
|
|
| |
Removed now defunct IdentifierSequence from the AST.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
to a file, making them easier to inspect and manipulate.
|
| |
|
|
|
|
| |
Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings.
Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions.
Fixed lack of operator resolution in custom attributes.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* The reads clause now needs to be self framing.
* The requires clause now needs to be framed by the reads clause.
* There are one-shot lambdas, with a single arrow, but they will probably be
removed.
* There is a {:heapQuantifier} attribute to quantifiers, but they will
probably be removed.
* Add smart handling of type variables
* Add < and > for datatype & type parameter
|
| |/
|
|
| |
the resolver and translator
|
Rustan Leino
Clément Pit--Claudel
Michael Lowell Roberts
Bryan Parno
Dan Rosén