| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
it. Don't use pretty warning signs since we can't diff them correctly in the
test output from the test run.
|
| |
|
|
|
| |
one exported view, but no exported view is marked as default, then it is an
error.
|
| |
|
|
| |
on context.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For the following situation
module LibA {
// ...things declared here...
}
module LibB {
// ...things declared here...
}
module R {
import opened LibA
// ...things declared here...
}
module S refines R {
import opened LibB
// ...declared here...
}
1. If module R declares a TopLevelDecl “G”, then we should report an error if S
attempts to declare an incompatible TopLevelDecl “G”. Dafny does this already.
2. If LibA declares a TopLevelDecl “G” but R does not directly declare any
TopLevelDecl G”, then we should also issue an error for any TopLevelDecl “G”
in S. This behavior is missing in Dafny.
3. If each of LibA and LibB declares some TopLevelDecl “G”, but neither R nor S
directly declares any TopLevelDecl “G”, then no error should be issued, and
any use of “G” in S should resolve to the “G” in LibA. This behavior is missing
in Dafny.
|
| | |
|
| |
|
|
| |
module.
|
| |
|
|
|
|
|
|
|
|
| |
1. A build failure caused by a method call before a contract was fixed.
2. An absolute path in an ".expect" file was changed to relative.
3. I eliminated the TopDecls and DeclModifiers non-terminals.
They were giving a warning from Coco/R about being deletable.
Instead I used repetition of the TopDecl or DeclModifier
non-terminals where they had been used. I think this is
also cleaner to talk about.
|
| |
|
|
|
|
| |
In the prior commit the ExternNegative2.dfy.expect file
was accidentally not included. It is needed in
order for that test to pass.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The 'extern' declaration modifier provides a more convenient
way of interfacing Dafny code with C# source files and
.Net DLLs.
We support an 'extern' keyword on a module, class, function method,
or method (cannot extern ghost). We check the CompileNames of
all modules to make sure there are no duplicate names.
Every Dafny-generated C# class is marked partial, so it can
potentially be extended.
The extern keyword could be accompanied by an optional string naming
the corresponding C# method/class to connect to. If not given
the name of the method/class is used.
An 'extern' keyword implies an {:axiom} attribute for functions
and methods, so their ensures clauses are assumed to be true
without proof.
In addition to the .dfy files, the user may supply
C# files (.cs) and dynamic linked libraries (.dll) on
command line. These will be passed onto the C# compiler,
the .cs files as sources, and the .dll files as references.
As part of this change the grammar was refactored some.
New productions are
- TopDecls - a list of top-level declarations.
- TopDecl - a single top-level declaration
- DeclModifiers - a list of declaration modifiers which are
either 'abstract', 'ghost', 'static', 'protected', or 'extern'.
They can be in any order and we diagnose duplicates.
In addition, since they are not all allowed in all contexts,
we check and give diagnostics if an DeclModifier appears
where it is not allowed.
|
| |
|
|
| |
the auto-triggers can be computed for ForallStmt.
|
| | |
|
| |
|
|
| |
it does not depend on the order they appeared.
|
| |
|
|
| |
protected predicated in cross-module calls) like in other places.
|
| |
|
|
|
| |
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)
|
| |
|
|
|
|
| |
itself,
as well as the signature and body of other functions.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
existential if guards.
Fixed bugs in ghost checks involving comprehensions and attributes.
Added SubstituteBoundedPool method.
|
| |
|
|
| |
of "if" statements.
|
| | |
|
| |
|
|
|
|
|
| |
predicates/lemmas (this fixes an item from the wishlist).
Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?).
Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1].
|
| |
|
|
| |
Moved all bounds discovery to resolution pass 1.
|
| |
|
|
|
|
| |
pass 0.
Fixed resolution of specification components of alternative loops.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
The issues here are mostly with induction (wrt. to trigger selection and
quantifier splitting) and with expressions like P(i, j-1) where no good choices
are available.
|
| | |
| |
| |
| |
| | |
We already have separate tests for those, and we want the output to be the same
with and without /autoTriggers.
|
| |/
|
|
| |
Dafny emacs mode
|
| | |
|
| | |
|
| |
|
|
|
|
| |
We can't prove `exists b: bool :: b || !b` when splitting is enabled, at least
for now, and there's already a separate test for that particular issue in
wishlist/
|
| |
|
|
| |
locations.
|
| |\ |
|
| | | |
|
| | |\
| |/
|/| |
|
| |\ \ |
|
| | |/ |
|
| | | |
|
| | |\
| |/
|/|
| |
| | |
Changes that were needed included preventing the InductionRewriter from
iterating on a SplitQuantifier and using the new error reporting engine.
|
| | | |
|
| | |
| |
| |
| | |
This new version will include a cleaner pipeline, and trigger splitting.
|
qunyanm
Richard L. Ford
Bryan Parno
Clément Pit--Claudel