summaryrefslogtreecommitdiff
path: root/Test/dafny1/SeparationLogicList.dfy
Commit message (Collapse)AuthorAge
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* Frame expressions are now checked to be well formed.Gravatar Rustan Leino2013-02-13
| | | | (A nice consequence of this is that the method IsTotal is no longer needed.)
* Dafny: retired the "call" keywordGravatar Rustan Leino2011-05-26
|
* Dafny: Axiom about inverting a set union operation, similar to the recent ↵Gravatar rustanleino2010-07-09
ones added for sequence concatenation. The new SeparationLogicList example profits from this axiom.