| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
empty.
|
|
|
|
| |
between a module and its refinement base.
|
|
|
|
| |
bound as undetermined so that iteration will continue.
|
| |
|
| |
|
| |
|
|
|
|
| |
collectors.
|
|
|
|
| |
collide with the names of its formals.
|
| |
|
|
|
|
| |
in MakeAbstractSignature.
|
|
|
|
| |
merge #24
|
|
|
|
| |
trying to substitute the nested CasePattern with the BoundVar.
|
|\ |
|
| | |
|
|/
|
|
| |
the auto-triggers can be computed for ForallStmt.
|
|
|
|
| |
occurrence of Set/MapComprehension when translating it to c#.
|
|
|
|
| |
LiteralExpr, write out its type instead.
|
|
|
|
| |
function and connect with Apply1 of the function.
|
| |
|
|\ |
|
| | |
|
| |
| |
| |
| |
| | |
swap them when the expr is first created in parser or for calcstmt. This
avoids problems of operands being swapped again when the expr is copied.
|
| |
| |
| |
| |
| | |
need exclude the private terms (the ones that includes the quantifier expr's bv)
from it exported terms.
|
|\| |
|
| | |
|
| |
| |
| |
| | |
DatatypeUpdateExpr if ResovedExpression is not null.
|
| |
| |
| |
| |
| |
| | |
method that is generated by LetExpr. Change the compiler so that each stmt
writes to its own buffer before add it to the program's buffer so that we can
insert the above mentioned copy instruction before the stmt.
|
| | |
|
| |
| |
| |
| | |
it does not depend on the order they appeared.
|
|/
|
|
| |
version that is less than 3.
|
|
|
|
| |
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.
|