summaryrefslogtreecommitdiff
path: root/Test/dafny0/TypeTests.dfy
Commit message (Expand)AuthorAge
* improved and fixed compilation and resolution of assign-such-that statementsGravatar Rustan Leino2012-10-05
* Dafny: deal with equality-support issues in refinementsGravatar Unknown2012-06-22
* Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to c...Gravatar Unknown2012-06-13
* Dafny: removed support for assigning to an array-range (that is, an assignmen...Gravatar Rustan Leino2011-10-26
* Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;"Gravatar Rustan Leino2011-05-28
* Dafny: permanently changed the syntax of "datatype" declarations to what prev...Gravatar Rustan Leino2011-05-27
* Dafny: retired the "call" keywordGravatar Rustan Leino2011-05-26
* Dafny:Gravatar Rustan Leino2011-05-21
* Dafny: added type "nat"Gravatar Rustan Leino2011-04-19
* Dafny: Allow field selections and array-element selection as LHSs of assignme...Gravatar Unknown2011-04-05
* Dafny: Added support for an initializing call as part of the new-allocation s...Gravatar rustanleino2011-03-27
* Dafny:Gravatar rustanleino2010-09-17
* Dafny:Gravatar rustanleino2010-07-06
* Dafny:Gravatar rustanleino2010-05-21
* Dafny: Added stratosphere tests for datatypes--that is, it is now checked th...Gravatar rustanleino2010-03-11
* * Added decreases clauses to functionsGravatar rustanleino2009-11-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 15:34:08 +0000