| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Beefed up loop invariant to prove a functional postcondition in a test case. |  Rustan Leino | 2012-11-24 |
| | | |||
| * | Test/dafny1/KatzManna.dfy: Changed mocked up matrix class to use Dafny's ↵ |  rustanleino | 2010-10-27 |
| | | | | | built-in array2 class. | ||
| * | Dafny: | rustanleino | 2010-06-24 |
| * For every loop decreases clause N, generate a free loop invariant N <= N0, where N0 is the value of N just before the loop. * Added Test/dafny1/KatzManna.dfy, which contains the 3 programs (and their termination annotations) from the Katz and Manna 1975 paper "A closer look at termination" (which benefits from the feature above). | |||
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |