{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T22:14:58Z","timestamp":1761948898977,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We propose a simple imperative programming language, ERC, that features\narbitrary real numbers as primitive data type, exactly. Equipped with a\ndenotational semantics, ERC provides a formal programming language-theoretic\nfoundation to the algorithmic processing of real numbers. In order to capture\nmulti-valuedness, which is well-known to be essential to real number\ncomputation, we use a Plotkin powerdomain and make our programming language\nsemantics computable and complete: all and only real functions computable in\ncomputable analysis can be realized in ERC. The base programming language\nsupports real arithmetic as well as implicit limits; expansions support\nadditional primitive operations (such as a user-defined exponential function).\nBy restricting integers to Presburger arithmetic and real coercion to the\n`precision' embedding $\\mathbb{Z}\\ni p\\mapsto 2^p\\in\\mathbb{R}$, we arrive at a\nfirst-order theory which we prove to be decidable and model-complete. Based on\nsaid logic as specification language for preconditions and postconditions, we\nextend Hoare logic to a sound (w.r.t. the denotational semantics) and\nexpressive system for deriving correct total correctness specifications.\nVarious examples demonstrate the practicality and convenience of our language\nand the extended Hoare logic.<\/jats:p>","DOI":"10.46298\/lmcs-20(2:17)2024","type":"journal-article","created":{"date-parts":[[2024,6,24]],"date-time":"2024-06-24T12:40:10Z","timestamp":1719232810000},"source":"Crossref","is-referenced-by-count":3,"title":["Semantics, Specification Logic, and Hoare Logic of Exact Real Computation"],"prefix":"10.46298","volume":"Volume 20, Issue 2","author":[{"given":"Sewon","family":"Park","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franz","family":"Brau\u00dfe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pieter","family":"Collins","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"SunYoung","family":"Kim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michal","family":"Kone\u010dn\u00fd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gyesik","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Norbert","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eike","family":"Neumann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Norbert","family":"Preining","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Ziegler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2024,6,24]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/13822\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/13822\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,24]],"date-time":"2024-06-24T12:40:10Z","timestamp":1719232810000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/7557"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,24]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(2:17)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"1608.05787v8","asserted-by":"subject"},{"id-type":"arxiv","id":"1608.05787v7","asserted-by":"subject"},{"id-type":"arxiv","id":"1608.05787v6","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1608.05787","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1608.05787","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,6,24]]},"article-number":"7557"}}