| Commit message (Expand) | Author | Age |
* | Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports. | qunyanm | 2016-02-05 |
* | Fix issue 117. Generate an error when the "opened" of an import doesn't match | qunyanm | 2016-01-08 |
* | Parsing and pretty printing of the new "existential guards" of the two kinds ... | leino | 2015-10-03 |
* | merged IronDafny updates. two unit tests related to traits do not pass if ENA... | Michael Lowell Roberts | 2015-09-21 |
* | Refactor the error reporting code | Clément Pit--Claudel | 2015-08-18 |
* | Allow forall statements in refinements | leino | 2015-07-31 |
* | multiple changes... | Michael Lowell Roberts | 2015-07-02 |
* | Add an infinite set collection type. | qunyanm | 2015-05-29 |
* | Added "inductive lemma" methods | leino | 2015-05-07 |
* | Added inductive predicates | leino | 2015-05-06 |
* | This changeset changes the default visibility of a function/predicate body ou... | leino | 2015-03-09 |
* | Added 'protected' keyword (syntax) | leino | 2015-03-07 |
* | Add imap type, which is like map but may have have infinite size | chrishaw | 2015-02-26 |
* | Fixed an encoding bug for newtypes (this fixes Issue #50) | Rustan Leino | 2015-01-27 |
* | Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, s... | leino | 2015-01-23 |
* | Language change: All functions and methods declared lexically outside any cla... | leino | 2014-12-12 |
* | Fixed some issues with assignments in refinements, both soundness bugs in pre... | leino | 2014-12-02 |
* | 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 |