| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
| |
error
if more than one method is so annotated. For that method, the usual restrictions
for "main" apply, but it is allowed to take ghost arguments, and it is allowed
to have preconditions. This lets the programmer add some explicit assumptions
about the outside world, modeled, for example, via ghost parameters.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
collide with the names of its formals.
|
| |
|
|
| |
occurrence of Set/MapComprehension when translating it to c#.
|
| |
|
|
| |
LiteralExpr, write out its type instead.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
existential if guards.
Fixed bugs in ghost checks involving comprehensions and attributes.
Added SubstituteBoundedPool method.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
| |
ENABLE_IRONDAFNY is defined but this isn't critical and will be addressed shortly.
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | |\
| |/
|/|
| |
| | |
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.
|
| |/ |
|
| | |
|
| |
|
|
| |
at least for some common expressions.
|
| |
|
|
|
| |
rather than xor. The latter produces pessimal performance if the
datatype contains duplicate data.
|
| | |
|
| | |
|
| |
|
|
| |
or == for equality testing.
|
| |
|
|
| |
functions/methods don't work yet)
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
with type parameters).
Resolve ClassDecl.TraitsTyp as types.
Moved declaration of TraitParent and NoTraitAtAll to prelude.
|
| |
|
|
| |
class when determining whether a method named Main() is the program entry.
|
| |
|
|
| |
have a unique value
|
| |
|
|
| |
Fixed comments in some test cases.
|
| |
|
|
| |
program is modified (to help with fine-grained caching)
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
use native C# representation of small integer newtypes.
Examples:
newtype{:nativeType "byte"} byte = i:int | 0 <= i < 0x100
newtype{:nativeType "sbyte"} sbyte = i:int | -0x80 <= i < 0x80
newtype{:nativeType "ushort"} uint16 = i:int | 0 <= i < 0x10000
newtype{:nativeType "short"} int16 = i:int | -0x8000 <= i < 0x8000
newtype{:nativeType "uint"} uint32 = i:int | 0 <= i < 0x100000000
newtype{:nativeType "int"} int32 = i:int | -0x80000000 <= i < 0x80000000
newtype{:nativeType "ulong"} uint64 = i:int | 0 <= i < 0x10000000000000000
newtype{:nativeType "long"} int64 = i:int | -0x8000000000000000 <= i < 0x8000000000000000
newtype month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise BigInteger
newtype{:nativeType} month = i:int | 0 <= i < 12 // same as {:nativeType true}
newtype{:nativeType true} month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise error
newtype{:nativeType false} month = i:int | 0 <= i < 12 // use BigInteger
newtype{:nativeType "uint"} month = i:int | 0 <= i < 12 // use C# uint type if possible, otherwise error
newtype{:nativeType} even20 = i:int | 0 <= i < 20 && (i % 2 == 0) // nativeTypes need not be contiguous
newtype{:nativeType} even10 = i:even20 | i < 10 // nativeTypes can inherit constraints from other nativeTypes
|
| | |
|
| |
|
|
| |
- a class can now extend more than one traits
|
| |
|
|
| |
- added one more test
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
qunyanm
Richard L. Ford
Michael Lowell Roberts
Clément Pit--Claudel
Bryan Parno
Reza Ahmadi