summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
...
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
* Did some refactoring of the Dafny drivers.Gravatar wuestholz2013-06-03
* Minor change to a project fileGravatar wuestholz2013-05-30
* Minor change to a project fileGravatar wuestholz2013-05-30
* Minor change to a project fileGravatar wuestholz2013-05-30
* Changed the Dafny driver to report traces for time outs and out of memory.Gravatar wuestholz2013-05-30
* MergeGravatar Rustan Leino2013-05-28
|\
| * DafnyExtension: minor changesGravatar wuestholz2013-05-27
| * DafnyExtension: Fixed an issue (error list wasn't cleared after closing buffe...Gravatar wuestholz2013-05-27
| * DafnyExtension: Added a button to the menu for stopping/starting the verifier.Gravatar wuestholz2013-05-26
| * DafnyExtension: Added menu for invoking specific Dafny functionality (e.g., c...Gravatar wuestholz2013-05-23
* | Allow more tail calls, on account of considering non-loop aggregate statement...Gravatar Rustan Leino2013-05-21
| * Minor change to a project fileGravatar wuestholz2013-05-21
| * Minor change to a project fileGravatar wuestholz2013-05-21
* | Fixed some omitted cases in Substitute (and added "assume false" to catch any...Gravatar Rustan Leino2013-05-21
* | Fixed bug, where prefix predicate was not included in CheckTypeInference visitorGravatar Rustan Leino2013-05-21
| * Minor change to a project fileGravatar wuestholz2013-05-21
| * Minor change to a project fileGravatar wuestholz2013-05-21
| * Updated several project files.Gravatar wuestholz2013-05-21
|/
* In Visual Studio interface, highlight variable definitions of let expressionsGravatar Rustan Leino2013-05-12
* Made the semi-colon after "type" and "module" declarations optional.Gravatar Rustan Leino2013-05-10
* Fix bug in substitution into let-such-that expressionsGravatar Rustan Leino2013-05-10
* When inlining the body of a predicate (in a proof obligation--via TrSplitExpr),Gravatar Rustan Leino2013-04-24
* Fixed (completeness) bug in translation of automatic induction--previously, t...Gravatar Rustan Leino2013-04-19
* Make semi-colon after datatype/codatatype declaration optional (in the future...Gravatar Rustan Leino2013-04-19
* Deleted a non-keywordGravatar Rustan Leino2013-04-04
* Refactored some resolution stages to make use of VisitorsGravatar Rustan Leino2013-04-02
* Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, ...Gravatar Rustan Leino2013-04-01
* Fixed compilation of assign-such-that for the multi-variable case where some ...Gravatar Rustan Leino2013-03-29
* The "choose" statement, hacky and specialized as it was, is now gone. Use th...Gravatar Rustan Leino2013-03-27
* Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more useful ...Gravatar Rustan Leino2013-03-27
* Compilation of (many common) assign-such-that statements.Gravatar Rustan Leino2013-03-26
* Suppress compiler warnings about unreferenced labels (I hope all .NET platfor...Gravatar Rustan Leino2013-03-26
* Type-inference support for cardinality operatorGravatar Rustan Leino2013-03-26
* MergeGravatar Rustan Leino2013-03-25
|\
* | Beefed up assign/let-such-that to generate possible witnesses for set/multise...Gravatar Rustan Leino2013-03-25
| * First take on set, multiset and map cardinality.Gravatar Nadia Polikarpova2013-03-22
|/
* Minor code cleanup.Gravatar Nadia Polikarpova2013-03-21
* Bumped version to 1.6.3.00320, to appear on rise4funGravatar Rustan Leino2013-03-20
* MergeGravatar Nadia Polikarpova2013-03-20
|\
* | Finished support for ==# in calc, changed Paulson example to use it.Gravatar Nadia Polikarpova2013-03-20
| * Added multiset update.Gravatar Nadia Polikarpova2013-03-20
| * Added multiset indexing.Gravatar Nadia Polikarpova2013-03-20
|/
* Added some data structure to support ==# in calculations.Gravatar Nadia Polikarpova2013-03-20
* Updated version to 1.6.2.00318Gravatar Rustan Leino2013-03-18
* MergeGravatar Rustan Leino2013-03-15
|\
* | Fixed yield statement to process its arguments.Gravatar Rustan Leino2013-03-15