| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Changed copyright date to include 2016.
|
| | |
|
| |
|
|
| |
static field and not initialized correctly. Make it an instance field instead.
|
| |
|
|
| |
context and less in an assert.
|
| |
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
| |
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.
|
| |\ |
|
| | |
| |
| |
| |
| | |
derived these predicates. More things can now be verified (including the
problem reported in Issue #49).
|
| | | |
|
| | |
| |
| |
| | |
until the editor is idle for 5 second.
|
| |/
|
|
| |
declared outside the enclosing match.
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
- various peephole optimizations of formulas, to generate fewer tautologies
- removed unused bound variables in CanCall quantifications (this addresses Issue #135)
- added type- and precondition-antecedent in quantified CanCall assumption for lambda expressions, thus fixing an unsoundness
|
| | |
| |
| |
| | |
"case" of a match statement and match expression.
|
| | | |
|
| |/ |
|
| |
|
|
| |
function is invoked inside an "Old" expression.
|
| | |
|
| |
|
|
| |
as int instead of bool.
|
| | |
|
| |
|
|
| |
a class is referenced.
|
| |
|
|
| |
boogie function calls with "Lit" function.
|
| |
|
|
| |
as candidates for triggers.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
expression from
// CanCall[[ var b :| RHS(b,g); Body(b,g,h) ]] =
// (forall b0,b1 :: typeAntecedent ==>
// CanCall[[ RHS(b,g) ]] &&
// (RHS(b,g) ==> CanCall[[ Body(b,g,h) ]]) &&
// $let$canCall(b,g))
to
// CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] =
// $let$canCall(g) &&
// CanCall[[ Body($let$b0(g), $let$b1(g), h) ]]
|
| |
|
|
|
|
|
|
| |
instantiate all it arguments, don't stop as soon as one instantiable constructor
is found. Instead, figure out all instantiable constructors and then pick the
best among these. A simple and reasonable "best" is an instantiable constructor
that requires a minimal number of already constructed type arguments, and to
break ties among these, pick the first one listed.
|
| | |
|
| |
|
|
| |
module.
|
| |
|
|
|
| |
The prior change did not work for people who had their
setup using the previous values.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
empty.
|
| |
|
|
|
|
| |
half a second, but delay calling Dafny resolver until the text buffer hasn't
been changed for 5 seconds. Also save the parsing result from TokenTagger in
ITextBuffer's property instead of in a static field.
|
| |
|
|
| |
that they don't show up in the VS IDE
|
| |
|
|
| |
between a module and its refinement base.
|
| |
|
|
| |
bound as undetermined so that iteration will continue.
|
| |
|
|
|
|
|
|
| |
are inherited
from the overridden method and Code Contracts will copy those preconditions to make sure
the right run-time checking happens; when Code Contracts finds preconditions on overrides,
it emits warnings).
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- cache scan results so it can be shared between different instances of
DafnyTokenTagger
- Instead of rescanning the whole text buffer upon a text change, only rescan
the text span that the text change is in.
- set the timer to half a second to match the comment at the beginnig of
the file. The event change are only passed along to Dafny when the user stop
typing for half a second.
- Change framework dependence so the project can work with version 4.5 and
higher.
|
| | |
|
| |
|
|
| |
collectors.
|
| |
|
|
|
|
|
|
| |
expressions to get the attributes for the forallstmt, which is flawed since the
forallexpr could have been splitted into different subquantifiers each with
different triggers. PrintExpression already knows how to print out
splitted forall expressions, so we use it to print the resolved forall
expressions instead.
|
| |
|
|
| |
collide with the names of its formals.
|
| |
|
|
| |
in MakeAbstractSignature.
|
| |
|
|
| |
trying to substitute the nested CasePattern with the BoundVar.
|
| |
|
|
|
|
|
| |
code introduced
with bug fix 103 and tripped over with the /rprint and /autoTriggers:1 flags used in the new
dafny4/UnionFind.dfy test).
|
| |\ |
|
| | | |
|
leino
Richard L. Ford