summaryrefslogtreecommitdiff
path: root/Test/dafny1/PriorityQueue.dfy
Commit message (Collapse)AuthorAge
* Dafny: Translate general LHSs for var and := (not yet for call, no ↵Gravatar Rustan Leino2011-05-30
| | | | compilation yet)
* Dafny: retired the "call" keywordGravatar Rustan Leino2011-05-26
|
* Dafny: Allow field selections and array-element selection as LHSs of ↵Gravatar Unknown2011-04-05
| | | | assignments where RHS is not just an expression
* 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