| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
module.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
of "if" statements.
|
| |
|
|
|
| |
The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.
|
| |
|
|
|
|
|
| |
If /useBasenameForFilename is specified, tokens just contain file names, which
is not enough to locate included files.
Solution based on Rustan's advice.
|
| |
|
|
|
| |
- fix for requirement inheritance in refinement.
- minimimally viable implementation of exclusive refinement feature.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
i.e., how many times Z3 is permitted to unfold it's definition. The
new {:fuel} annotation can be added to the function itself, it which
case it will apply to all uses of that function, or it can overridden
within the scope of a module, function, method, iterator, calc, forall,
while, assert, or assume. The general format is:
{:fuel functionName,lowFuel,highFuel}
When applied as an annotation to the function itself, omit functionName.
If highFuel is omitted, it defaults to lowFuel + 1.
The default fuel setting for recursive functions is 1,2. Setting the fuel higher,
say, to 3,4, will give more unfoldings, which may make some proofs go through
with less programmer assistance (e.g., with fewer assert statements), but it may
also increase verification time, so use it with care. Setting the fuel to 0,0 is
similar to making the definition opaque, except when used with all literal arguments.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
expression.
|
| |
|
|
| |
parameters
|
| |
|
|
|
|
| |
supported a GREEDY annotation)
Don't allow colons with no intervening expressions in sequence-slicing expression
|
| | |
|
| |
|
|
|
| |
Disallow empty modifies/reads clauses (this eliminates some LL(1) warnings)
Require modify statement to take a nonempty list of frame expressions
|
| | |
|
| |
|
|
|
| |
e.g., Ironclad's calls to assembly instructions.
Also fixed what appeared to be a bug in the Makefile for invoking Coco
|
| |
|
|
|
|
| |
are written as numeric strings). The
underscores have no semantic meaning, but can help a human parse the numbers.
|
| |
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
| |
Added parsing of constraints (beyond parsing is yet to come)
|
| |
|
|
| |
Fixed bug in type checking for integer division.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* 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
|
| |/
|
|
|
|
| |
-possibility to declare traits in Dafny
-possibility to extend a class by a trait
-possibility to override body-less methods
|
| |
|
|
| |
braces around the cases are now supported for both and are optional for both
|
| |
|
|
| |
In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
|
| |
|
|
| |
-> "prefix lemma")
|
| | |
|
| |
|
|
|
| |
to another Dafny file. That file's functions and methods are included but not checked.
This is intended to support incremental verification on a per-file basis.
|
| | |
|
| |
|
|
| |
a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
the assign-such-that statement instead. For example: x :| x in S;
|
| | |
|
| | |
|
| |
|
|
| |
around the bound variables optional.
|
| | |
|
| |
|
|
| |
Added syntactic support for codatatype #-form equalities.
|
| |
|
|
| |
'yields' for an iterator
|
qunyanm
Richard L. Ford
Clément Pit--Claudel
Michael Lowell Roberts
Bryan Parno
Dan Rosén
Reza Ahmadi
Nadia Polikarpova
Rustan Leino