summaryrefslogtreecommitdiff
path: root/Test/dafny0/AdvancedLHS.dfy
Commit message (Expand)AuthorAge
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* The "choose" statement, hacky and specialized as it was, is now gone. Use th...Gravatar Rustan Leino2013-03-27
* Added multiset from sequence axioms, removed array range RHSs. Fixed issue wi...Gravatar Jason Koenig2011-07-13
* Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;"Gravatar Rustan Leino2011-05-28
* Dafny: don't require parentheses in syntax of "choose" statementsGravatar Rustan Leino2011-04-05
* Dafny: Allow field selections and array-element selection as LHSs of assignme...Gravatar Unknown2011-04-05