diff options
| author |  rustanleino <unknown> | 2010-06-24 00:41:04 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-24 00:41:04 +0000 |
| commit | cf26b0336a404760302bd57eb822fa906105cf1d (patch) | |
| tree | 7043f794c473404d8895af7946c302e258dd1fd6 /Test/dafny1/Substitution.dfy | |
| parent | 67c07706d2b4ee941954301a0c18abfcf253384c (diff) | |
Dafny:
* 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).
Diffstat (limited to 'Test/dafny1/Substitution.dfy')
0 files changed, 0 insertions, 0 deletions