| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
class are now
automatically static, and fields are no longer allowed to be declared there. Stated
differently, all heap state must now be declared inside an explicitly declared class,
and functions and methods declared outside any class can be viewed as belonging to
the module. The motivating benefit of this change is to no longer need the 'static'
keyword when declaring a module of functions and methods.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
to use it.
|
| |
|
|
|
|
|
| |
where more type information is known
Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement.
Fixed numerous places where some recursive checks did not reach.
|
| |
|
|
| |
Changed the test output to make it easier to spot (in the console output) that everything passed with success or if there were any failures
|
| |
|
|
|
|
| |
Iter.dfy!)
Fixed migration issues
|
| |
|
|
| |
Z3 4.1.
|
| | |
|
| |
|
|
| |
.cs file with the new /spillTargetCode switch
|
| | |
|
| |
|
|
| |
avoid clashes with C# keywords, added switch in runtest scripts to turn on compilation
|
| |
|
|
| |
assignments where RHS is not just an expression
|
| |
|
|
|
|
|
|
|
|
|
| |
syntax. What you previously would have written like:
c := new C;
call c.Init(x, y);
you can now write as:
c := new C.Init(x, y);
|
| |
|
|
|
|
| |
Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction
Dafny: split expressions when proving function postconditions
Boogie and BVD: updated copyright year ranges
|
| |
|
|
| |
to "function" in a test case.
|
| |
|
|
|
| |
Dafny: Don't display "alloc" field in BVD
Chalice: Fixed error-message parsing error in VS mode
|
| | |
|
| |
|
|
| |
Dafny: Simplified VSComp2010/Problem4-Queens.dfy from using an inductive ghost-method lemmas to just using an assert
|
| |
|
|
|
|
| |
* 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
|
| |
|
Clément Pit--Claudel
leino
Rustan Leino
Unknown
Unknown