| Commit message (Expand) | Author | Age |
|---|
| * | Fixed bug in tuples |  leino | 2015-04-24 |
| * | Allow let-such-that expression to be compiled, provided that they provably ha... | leino | 2015-03-13 |
| * | Fixed bug in resolution of illegal programs. | leino | 2015-03-10 |
| * | Stop pretty-print from emitting deprecated semi-colons. | qunyanm | 2015-03-05 |
| * | When ambiguous references all resolve to the same declaration, don't complain | leino | 2015-01-09 |
| * | Language change: All functions and methods declared lexically outside any cla... | leino | 2014-12-12 |
| * | Snapshot, to be continued | leino | 2014-12-02 |
| * | Fixed bug where resolution was overly restrictive with ghost variables appear... | leino | 2014-11-19 |
| * | Disallow automatic completion of type arguments to the LHS of datatype declar... | leino | 2014-10-28 |
| * | Stricter rules about that types need to be completely resolved. | leino | 2014-10-08 |
| * | Support for non-constrained derived types ("new types"). | leino | 2014-08-21 |
| * | 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 |
| |/ |
|
| * | Refactor resolver, and really allow reads to take fields of type A -> set<obj> |  Dan Rosén | 2014-08-15 |
| * | Resolved further merge issues | leino | 2014-08-05 |
| * | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in th... | leino | 2014-08-02 |
| * | Allow an arbitrary-type to take type parameters | Rustan Leino | 2014-07-15 |
| * | Added type synonyms. (No support yet for these in refinements.) | Rustan Leino | 2014-07-11 |
| * | Merge | Rustan Leino | 2014-07-08 |
| |\ |
|
| * | | Test cases for int<->real conversions | Rustan Leino | 2014-07-08 |
| | * | Allow array-type parameters to be filled in automatically. | leino | 2014-07-02 |
| |/ |
|
| * | Added tuples and tuple types. Syntax is the expected one, namely parentheses ... | Rustan Leino | 2014-06-27 |
| * | Added support for 'dirty' forall statements. | chmaria | 2014-06-03 |
| * | Set up the same test infrastructure as in Boogie. | wuestholz | 2014-05-29 |
| * | Fixed bug #32 dafny.codeplex.com. | Rustan Leino | 2014-04-15 |
| * | Changed an error from a verification error to a syntactic (resolution) error | Rustan Leino | 2014-04-04 |
| * | Added "modify" statement. | Rustan Leino | 2014-04-03 |
| * | Fixed problem with propagating allocation information about array elements. | Rustan Leino | 2014-03-20 |
| * | Added ghost let expressions. | Rustan Leino | 2014-01-05 |
| * | Allow calls to side-effect-free ghost methods from expressions | Rustan Leino | 2013-08-06 |
| * | Set up call-graph to keep track of edges between functions and methods. (To ... | Rustan Leino | 2013-08-04 |
| * | Introduced keywords "lemma" (like a "ghost method", but not allowed to have a... | Rustan Leino | 2013-08-02 |
| * | Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, ... | Rustan Leino | 2013-04-01 |
| * | Disallow allocations in ghost contexts | Rustan Leino | 2013-03-06 |
| * | Added side-effects and control-flow checks in hints. |  Nadia Polikarpova | 2013-03-05 |
| * | Report error if type of a quantified variable cannot be inferred | Rustan Leino | 2013-02-11 |
| * | Translate let-such-that expressions |  Rustan Leino | 2013-01-22 |
| * | fixed and improved scheme for inferring type parameters | Rustan Leino | 2012-10-19 |
| * | improved and fixed compilation and resolution of assign-such-that statements | Rustan Leino | 2012-10-05 |
| * | Support default (which, here, means nameless) class-instance constructors | Rustan Leino | 2012-10-05 |
| * | Bugfix in the translation of calc statements (oops), added more resolution an... | Nadia Polikarpova | 2012-09-21 |
| * | Added tests for parsing and resolution of calc statements | Nadia Polikarpova | 2012-09-21 |
| * | Dafny: allow various forms of leaving off type arguments in declarations | Rustan Leino | 2012-02-16 |
| * | Dafny: don't allow ghost expressions in print statements | Rustan Leino | 2012-01-03 |
| * | Dafny: implemented the wellformedness check that datatype destructors are onl... | Rustan Leino | 2011-11-11 |
| * | Dafny: fix resolution crash (using multi-dimensional arrays in loop alternative) | Rustan Leino | 2011-08-03 |
| * | Dafny: added implicit datatype query fields and datatype destructor fields | Rustan Leino | 2011-06-05 |
| * | Dafny: added constructors | Rustan Leino | 2011-05-28 |
| * | Dafny: added chaining operators | Rustan Leino | 2011-05-27 |
leino
Dan Rosén
Nadia Polikarpova
Rustan Leino