diff options
| author | Brian Campbell | 2019-07-31 15:16:17 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-07-31 16:43:51 +0100 |
| commit | 2b64d1215c7b77d8cc37a4ab3c9ff2cc5a07e12b (patch) | |
| tree | b791c70a987fdad72fa7e1be15dea01f303fe32a /doc | |
| parent | 98cced7ef3cf89333e0e09d4ebf9ca3262b4e947 (diff) | |
Coq: reasoning for until loops
Loops measures are now abstracted over the variables so that they can be
used in proofs. Add total Hoare logic rules for until.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions