| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
|
| | |
|
| |
|
|
| |
a previous lemma
|
| |
|
|
|
|
|
| |
* implemented induction tactic for result-less, non-mutating ghost methods
* refine heuristics for determining if a variables is usefully passed to a recursive function
* disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy)
* added command-line flags /induction and /inductionHeuristic (everything is on by default)
|
| | |
|
| | |
|
| |
|
|
| |
functions/methods, and updated some test files accordingly (compare with changesets 1429 and 1366)
|
| |\ |
|
| | | |
|
| |/ |
|
| |
|
|
| |
body-less functions/methods
|
| |
|
|
| |
previously was an alternative syntax
|
| |
|
|
|
|
|
|
|
|
| |
* started rewriting parsing of qualified identifiers in expressions
* annoyingly, had to introduce AST nodes for concrete syntax
* previous syntax for invoking datatype constructors: #List.Cons(h, t)
new syntax: List.Cons(h, t)
or, if only one datatype has a constructor named Cons: Cons(h, t)
* Removed type parameters for datatype constructors from the grammar
* Helped Test/VSI-Benchmarks/b4.dfy along with a couple of assertions (previously, its proving performance was highly varied)
|
| | |
|
| |
|
|
| |
and) verifiable
|
|
|
* Support for induction over more than 1 variable
* Added many of the Rippling induction benchmarks
* Fixed bug in case handling
|
Rustan Leino
Jason Koenig