summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* renamed "abstract module" to "module facade"Gravatar Rustan Leino2012-10-22
* allow a refinement to introduce "return" statements, at the price of re-verif...Gravatar Rustan Leino2012-10-22
* combine {:autocontracts} and refinementGravatar Rustan Leino2012-10-21
* Disallow modifies clauses on comethodsGravatar Unknown2012-10-19
* fixed and improved scheme for inferring type parametersGravatar Rustan Leino2012-10-19
* Fixed compiler bug for "opened" importsGravatar Rustan Leino2012-10-18
* some code clean-upGravatar Rustan Leino2012-10-18
* Pass Boogie's new SoundLoopUnrolling parameterGravatar Rustan Leino2012-10-18
* Included "all cases of a datatype" property for method in-parameters (see htt...Gravatar Unknown2012-10-17
* MergeGravatar Unknown2012-10-17
|\
* | Added some axioms to try to recover boxed data. In particular, any element '...Gravatar Unknown2012-10-17
| * Updated HintPath's of DLL's in the building of DafnyExtensionGravatar Rustan Leino2012-10-17
* | Added/fixed decreases clauses that use multisets or maps.Gravatar Unknown2012-10-16
|/
* Change the encoding of proof certificates to make the two levels explicitGravatar Unknown2012-10-12
* Removed some old code for the defunct array-range assignmentsGravatar Rustan Leino2012-10-11
* Removed the old (though automatic) coinduction principleGravatar Rustan Leino2012-10-11
* New feature:Gravatar Rustan Leino2012-10-11
* improved and fixed compilation and resolution of assign-such-that statementsGravatar Rustan Leino2012-10-05
* Longer output lines to indicate failures in regression test suiteGravatar Rustan Leino2012-10-05
* Support default (which, here, means nameless) class-instance constructorsGravatar Rustan Leino2012-10-05
* Hover text for iterator declarations (and not for the methods they generate)Gravatar Rustan Leino2012-10-04
* More free antecedents when proving well-formedness of iterator specsGravatar Rustan Leino2012-10-04
* changed default decreases clause for functions with a reads clause: use the r...Gravatar Rustan Leino2012-10-04
* Fixed some build/migration issuesGravatar Rustan Leino2012-10-04
* Updates of various .sln and .*proj filesGravatar Rustan Leino2012-10-04
* Put all sources under \Source directoryGravatar Rustan Leino2012-10-04