| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
expression from
// CanCall[[ var b :| RHS(b,g); Body(b,g,h) ]] =
// (forall b0,b1 :: typeAntecedent ==>
// CanCall[[ RHS(b,g) ]] &&
// (RHS(b,g) ==> CanCall[[ Body(b,g,h) ]]) &&
// $let$canCall(b,g))
to
// CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] =
// $let$canCall(g) &&
// CanCall[[ Body($let$b0(g), $let$b1(g), h) ]]
|
| |
|
|
|
|
|
|
| |
expressions to get the attributes for the forallstmt, which is flawed since the
forallexpr could have been splitted into different subquantifiers each with
different triggers. PrintExpression already knows how to print out
splitted forall expressions, so we use it to print the resolved forall
expressions instead.
|
| |
|
|
|
|
|
| |
code introduced
with bug fix 103 and tripped over with the /rprint and /autoTriggers:1 flags used in the new
dafny4/UnionFind.dfy test).
|
| |
|
|
| |
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.
|
| | |
|
| |\
| |
| |
| |
| | |
Changes that were needed included preventing the InductionRewriter from
iterating on a SplitQuantifier and using the new error reporting engine.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| | |
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'.
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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)
}
|
| | |
|
| | |
|
| |
|
|
| |
so that printMode NoIncludes/NoGhost works
|
| |
|
|
|
|
|
| |
with type parameters).
Resolve ClassDecl.TraitsTyp as types.
Moved declaration of TraitParent and NoTraitAtAll to prelude.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
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
|
| |
|
|
| |
Finished refactoring of the recent name segments changes.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| | |
| |
| |
| | |
- a class can now extend more than one traits
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
| |
statements
|
| |
|
|
| |
Disallow backslash from being part of identifier names.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
| |
Cleaner printing of .reads and .requires members of the built-in arrow "classes".
|
| |
|
|
| |
along with a backward-compatibility warning message if such declarations are attempted
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Fixed bug in type checking for integer division.
|
| | |
|
| |\ |
|
qunyanm
Michael Lowell Roberts
Clément Pit--Claudel
Reza Ahmadi
Bryan Parno
Dan Rosén