summaryrefslogtreecommitdiff
path: root/Test/dafny1/PriorityQueue.dfy
Commit message (Expand)AuthorAge
* Dafny: allow definitions and uses of parameter-less predicates to go without ...Gravatar Rustan Leino2012-01-10
* Dafny: Translate general LHSs for var and := (not yet for call, no compilatio...Gravatar Rustan Leino2011-05-30
* Dafny: retired the "call" keywordGravatar Rustan Leino2011-05-26
* Dafny: Allow field selections and array-element selection as LHSs of assignme...Gravatar Unknown2011-04-05
* Dafny: added alternate version of PriorityQueueGravatar rustanleino2011-02-15
* Dafny: added ensures clauses to functionsGravatar rustanleino2011-02-02
* Dafny: Added Test/dafny1/PriorityQueue.dfyGravatar rustanleino2010-12-10