| 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.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
with duplicate array.Length functions in generated Boogie file.
|
|
|
|
| |
updated regression tests.)
|
|
|
|
| |
assignments where RHS is not just an expression
|
|
|
|
|
|
| |
* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation)
* Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays.
* Internally, this meant adding support for built-in classes and readonly fields
|
|
* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks
|