{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:25:08Z","timestamp":1759638308303,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,2,11]],"date-time":"2015-02-11T00:00:00Z","timestamp":1423612800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>In search for a foundational framework for reasoning about observable\nbehavior of programs that may not terminate, we have previously devised a\ntrace-based big-step semantics for While. In this semantics, both traces and\nevaluation (relating initial states of program runs to traces they produce) are\ndefined coinductively. On terminating runs, this semantics agrees with the\nstandard inductive state-based semantics. Here we present a Hoare logic\ncounterpart of our coinductive trace-based semantics and prove it sound and\ncomplete. Our logic subsumes the standard partial-correctness state-based Hoare\nlogic as well as the total-correctness variation: they are embeddable. In the\nconverse direction, projections can be constructed: a derivation of a Hoare\ntriple in our trace-based logic can be translated into a derivation in the\nstate-based logic of a translated, weaker Hoare triple. Since we work with a\nconstructive underlying logic, the range of program properties we can reason\nabout has a fine structure; in particular, we can distinguish between\ntermination and nondivergence, e.g., unbounded classically total search fails\nto be terminating, but is nonetheless nondivergent. Our meta-theory is entirely\nconstructive as well, and we have formalized it in Coq.<\/jats:p>","DOI":"10.2168\/lmcs-11(1:1)2015","type":"journal-article","created":{"date-parts":[[2015,5,18]],"date-time":"2015-05-18T07:33:27Z","timestamp":1431934407000},"source":"Crossref","is-referenced-by-count":11,"title":["A Hoare logic for the coinductive trace-based big-step semantics of While"],"prefix":"10.46298","volume":"Volume 11, Issue 1","author":[{"given":"Keiko","family":"Nakata","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1297-0579","authenticated-orcid":false,"given":"Tarmo","family":"Uustalu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2015,2,11]]},"reference":[{"key":"600:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/692\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/692\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:53:57Z","timestamp":1681242837000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/692"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,11]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-11(1:1)2015","relation":{"is-same-as":[{"id-type":"arxiv","id":"1412.6579","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1412.6579","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2015,2,11]]},"article-number":"692"}}