| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
operator on datatypes
Dafny: allow the well-formedness check of a function's specification to know that the function, on the current arguments, returns a value of the declared result type
|
| | |
|
| |
|
|
| |
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)
|
| |
|
|
|
|
| |
* added missing error checking for ghost-vs-physical contexts (e.g., use of the "old" keyword)
* check that arrays are not null when accessed
* added dafny1/FindZero.dfy test case
|
| |
|
Rustan Leino
Jason Koenig