| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
of "if" statements.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
|
| |
|
|
| |
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)
|
| |
|
|
| |
that every datatype has some value.
|
| |
|
|
|
|
|
|
| |
boolean-only if-then-else expressions)
Dafny: Added 'class' functions and methods (i.e., functions and methods with a receiver parameter)
Dafny grammar changes: Tthe 'use' keyword now goes before 'function' (akin to 'ghost' and 'class'), and quantifier triggers now go before the '::'
Dafny: Check for division-by-zero for both '/' and '%'
|
| |
|
|
| |
Included VSI-Benchmarks in standard tests.
|
| | |
|
| |
|
leino
Rustan Leino