| Commit message (Expand) | Author | Age |
* | Added types "char" and "string" (the latter being a synonym for "seq<char>"). | leino | 2014-10-20 |
* | Disallow parentheses-less declarations of predicates and co-predicates, along... | leino | 2014-08-27 |
* | Refactoring: renamed DerivedTypeDecl to NewtypeDecl | leino | 2014-08-26 |
* | Merge | leino | 2014-08-20 |
|\ |
|
* | | Start of derived types (aka "new types") | leino | 2014-08-20 |
| * | Change behavior of 'decreases *', which can be applied to loops and methods. ... | Rustan Leino | 2014-08-19 |
|/ |
|
* | Merge | Dan Rosén | 2014-08-11 |
|\ |
|
* | | Add higher-order-functions and some other goodies | Dan Rosén | 2014-08-11 |
| * | added trait feature: | Reza Ahmadi | 2014-07-18 |
|/ |
|
* | Renamed "arbitrary type" to "opaque type" | Rustan Leino | 2014-07-15 |
* | Support for type synonyms in refinements | Rustan Leino | 2014-07-14 |
* | Added type synonyms. (No support yet for these in refinements.) | Rustan Leino | 2014-07-11 |
* | Make reveal axioms from opaque functions quantify over layers | Dan Rosén | 2014-07-10 |
* | Fixed refinement of modify statements | Rustan Leino | 2014-04-04 |
* | Support the transition from "modify Frame;" to "modify Frame { Body }" by ref... | Rustan Leino | 2014-04-04 |
* | Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss t... | Rustan Leino | 2014-03-17 |
* | Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -... | Rustan Leino | 2014-02-23 |
* | Preliminary support for reals in Dafny specs. No compiler suport yet. | Bryan Parno | 2014-02-10 |
* | Produce hover text for many of the refinement omissions (i.e., "..." and the ... | Rustan Leino | 2014-01-31 |
* | Changed the iterator class hover text back to the iterator name (which is con... | Rustan Leino | 2013-12-20 |
* | Added an .EndTok for every statement. (Note, in some places, especially in V... | Rustan Leino | 2013-12-19 |
* | Refactored the calling of rewriters | Rustan Leino | 2013-12-11 |
* | Introduced keywords "lemma" (like a "ghost method", but not allowed to have a... | Rustan Leino | 2013-08-02 |
* | Renamed "parallel" statement to "forall" statement, and made the parentheses ... | Rustan Leino | 2013-03-06 |
* | Added Equals method on Type | Rustan Leino | 2013-02-20 |
* | renamed "abstract module" to "module facade" | Rustan Leino | 2012-10-22 |
* | allow a refinement to introduce "return" statements, at the price of re-verif... | Rustan Leino | 2012-10-22 |
* | combine {:autocontracts} and refinement | Rustan Leino | 2012-10-21 |
* | New feature: | Rustan Leino | 2012-10-11 |
* | Put all sources under \Source directory | Rustan Leino | 2012-10-04 |