summaryrefslogtreecommitdiff
path: root/Source/Dafny/Translator.cs
Commit message (Expand)AuthorAge
...
* Compile lambda functions and apply expressions, and change let expr compilationGravatar Dan Rosén2014-08-12
* MergeGravatar Dan Rosén2014-08-11
|\
* | Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
| * MergeGravatar leino2014-08-02
| |\
| * | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in th...Gravatar leino2014-08-02
|/ /
| * added trait feature:Gravatar Reza Ahmadi2014-07-18
|/
* Renamed "arbitrary type" to "opaque type"Gravatar Rustan Leino2014-07-15
* Allow an arbitrary-type to take type parametersGravatar Rustan Leino2014-07-15
* Support for type synonyms in refinementsGravatar Rustan Leino2014-07-14
* MergeGravatar Rustan Leino2014-07-11
|\
* | Added type synonyms. (No support yet for these in refinements.)Gravatar Rustan Leino2014-07-11
| * Don't assume can calls for quantifiersGravatar Dan Rosén2014-07-11
|/
* Make reveal axioms from opaque functions quantify over layersGravatar Dan Rosén2014-07-10
* Ignore checked-only and free-only split expressions in places where they "don...Gravatar Rustan Leino2014-07-09
* MergeGravatar Rustan Leino2014-07-08
|\
* | Implemented compilation of the int<->real conversions, and changed the resolu...Gravatar Rustan Leino2014-07-08
| * MergeGravatar Dan Rosén2014-07-07
| |\
| * | New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
| | * MergeGravatar leino2014-07-03
| | |\
| | * | Translate CanCallAssumption with the same fuel value as in the body of the fu...Gravatar leino2014-07-03
| | | * Changed "dummy" checksums to "stable" and added more tests for the verificati...Gravatar wuestholz2014-07-03
* | | | Fixed a crash in the translation of fresh(seq<T>).Gravatar Rustan Leino2014-07-02
| |_|/ |/| |
| | * MergeGravatar leino2014-07-01
| | |\ | |_|/ |/| |
* | | Added support for verifying Dafny program snapshots from the command-line.Gravatar wuestholz2014-07-01
| | * MergeGravatar leino2014-06-24
| | |\ | |_|/ |/| |
| | * MergeGravatar leino2014-06-24
| | |\
* | | | Make syntax of "match" expressions and "match" statements the same -- curly b...Gravatar Rustan Leino2014-06-24
| |/ / |/| |
* | | Invert LHS sub-expressions in forall assignment statements, which gives the o...Gravatar Rustan Leino2014-06-24
| | * MergeGravatar leino2014-06-16
| | |\ | |_|/ |/| |
| | * Add support doing computations over sequencesGravatar leino2014-06-16
* | | Specialized Lit function for int and real (leaving all other cases polymorphi...Gravatar Rustan Leino2014-06-10
| |/ |/|
* | Added support for 'dirty' forall statements.Gravatar chmaria2014-06-03
|/
* Add support for assumption variables.Gravatar wuestholz2014-04-21
* Members included from different files are now internally marked with an Inclu...Gravatar Rustan Leino2014-04-19
* Allow reals in decreases clausesGravatar Rustan Leino2014-04-08
* MergeGravatar Rustan Leino2014-04-04
|\
* | Also include lower set bounds (bounding a set from below) in witness guesses ...Gravatar Rustan Leino2014-04-04
* | Changed an error from a verification error to a syntactic (resolution) errorGravatar Rustan Leino2014-04-04
* | Added "modify Frame { Body }" statement.Gravatar Rustan Leino2014-04-04
* | Added "modify" statement.Gravatar Rustan Leino2014-04-03
| * Basic support for datatype-update syntatic sugarGravatar Bryan Parno2014-04-03
|/
* Reduced noise in BVD display of temporary variables of the translationGravatar Rustan Leino2014-03-24
* Propagate literals through equality operations.Gravatar Nada Amin2014-03-19
* MergeGravatar Rustan Leino2014-03-17
|\
* | Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss t...Gravatar Rustan Leino2014-03-17
* | AST refactoring:Gravatar Rustan Leino2014-03-17
| * Improve computations, in particular compositionality. Isolated useless litera...Gravatar Nada Amin2014-03-12
| * change computation weight to 3. Tests still pass.Gravatar Nada Amin2014-03-11
|/
* Refactored code for dealing with SCCs in the call graph.Gravatar Rustan Leino2014-02-24
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -...Gravatar Rustan Leino2014-02-23