| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
"case" of a match statement and match expression.
|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
| |
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.
|
| |
|
|
|
| |
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.
|
| | |
| |
| |
| |
| | |
The new error reporting system has a simpler interface, isn't tied to the
resolver, and contains error source information.
|
| |/ |
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
that Coco.exe is now included in boogiepartners.
|
| |/
|
|
|
| |
There now is one main entry point for reporting errors, warnings, or
information. Next step is to make the VS extension use that.
|
| |
|
|
|
|
|
| |
If /useBasenameForFilename is specified, tokens just contain file names, which
is not enough to locate included files.
Solution based on Rustan's advice.
|
| |
|
|
|
|
|
|
|
| |
Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we
print tokens, we need to decrement the column number. This was done for resolver
errors, but not for verification or parsing errors. In addition, parsing errors
were inconsistent with resolution errors case-wise.
Unfortunately, the fix affects the output of many tests.
|
| |
|
|
|
| |
- diabled error message related to ensures clauses requiring function bodies in the case of abstract modules.
- fixed bug in similar error message related to bodyless methods in abstract modules.
|
| |\ |
|
| | |
| |
| |
| |
| | |
Fixed resolution bug where some type arguments were not checked to have been determined.
Fixed resolution bugs where checking for equality-supporting types was missing.
|
| |/ |
|
| |
|
|
|
| |
- 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.
|
| |
|
|
|
|
|
| |
Mono currently does not implement support for BigInteger.Parse, so use Int64 if
possible, and throw the same error as was previously returned otherwise. This is
not too much of a problem in practice, because most of the integers that we
actually come across in real-life source files seem to fit in an Int64.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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)
}
|
| | |
|
| | |
|
| |
|
|
| |
from included files
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
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
|
| |
|
|
| |
changes introduced in changeset c56031307ac1
|
| |
|
|
| |
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.
|
| |
|
|
| |
Corrected merge
|
| |\ |
|
| | | |
|
| | |
| |
| |
| | |
- a class can now extend more than one traits
|
| | | |
|
| |/ |
|
| |
|
|
| |
expression.
|
| |
|
|
| |
parameters
|
qunyanm
Richard L. Ford
Clément Pit--Claudel
Michael Lowell Roberts
Bryan Parno
Reza Ahmadi