summaryrefslogtreecommitdiff
path: root/Source/Dafny/Rewriter.cs
Commit message (Collapse)AuthorAge
* Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr;Gravatar Unknown2012-03-15
|
* Dafny: added ghost modules (the meaning is simply that such a module will ↵Gravatar Rustan Leino2012-03-07
| | | | | | | not be compiled) Dafny: improved :autocontracts heuristic for detecting "simple query method" Dafny: fixed some bugs
* Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic ↵Gravatar Unknown2012-03-05
specifications