DC Field | Value | Language |
---|---|---|
dc.contributor.author | Park, Sewon | ko |
dc.contributor.author | Brauße, Franz | ko |
dc.contributor.author | Collins, Pieter | ko |
dc.contributor.author | Kim, SunYoung | ko |
dc.contributor.author | Konečný, Michal | ko |
dc.contributor.author | Lee, Gyesik | ko |
dc.contributor.author | Müller, Norbert | ko |
dc.contributor.author | Neumann, Eike | ko |
dc.contributor.author | Preining, Norbert | ko |
dc.contributor.author | Ziegler, Martin | ko |
dc.date.accessioned | 2024-06-25T03:00:05Z | - |
dc.date.available | 2024-06-25T03:00:05Z | - |
dc.date.created | 2024-06-25 | - |
dc.date.issued | 2024-06 | - |
dc.identifier.citation | Logical Methods in Computer Science, v.20, no.2 | - |
dc.identifier.issn | 1860-5974 | - |
dc.identifier.uri | http://hdl.handle.net/10203/320001 | - |
dc.description.abstract | <jats:p>We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin powerdomain and make our programming language semantics computable and complete: all and only real functions computable in computable analysis can be realized in ERC. The base programming language supports real arithmetic as well as implicit limits; expansions support additional primitive operations (such as a user-defined exponential function). By restricting integers to Presburger arithmetic and real coercion to the `precision' embedding $\mathbb{Z}\ni p\mapsto 2^p\in\mathbb{R}$, we arrive at a first-order theory which we prove to be decidable and model-complete. Based on said logic as specification language for preconditions and postconditions, we extend Hoare logic to a sound (w.r.t. the denotational semantics) and expressive system for deriving correct total correctness specifications. Various examples demonstrate the practicality and convenience of our language and the extended Hoare logic.</jats:p> | - |
dc.language | English | - |
dc.publisher | Centre pour la Communication Scientifique Directe (CCSD) | - |
dc.title | Semantics, Specification Logic, and Hoare Logic of Exact Real Computation | - |
dc.type | Article | - |
dc.type.rims | ART | - |
dc.citation.volume | 20 | - |
dc.citation.issue | 2 | - |
dc.citation.publicationname | Logical Methods in Computer Science | - |
dc.identifier.doi | 10.46298/lmcs-20(2:17)2024 | - |
dc.contributor.localauthor | Ziegler, Martin | - |
dc.contributor.nonIdAuthor | Park, Sewon | - |
dc.contributor.nonIdAuthor | Brauße, Franz | - |
dc.contributor.nonIdAuthor | Collins, Pieter | - |
dc.contributor.nonIdAuthor | Kim, SunYoung | - |
dc.contributor.nonIdAuthor | Konečný, Michal | - |
dc.contributor.nonIdAuthor | Lee, Gyesik | - |
dc.contributor.nonIdAuthor | Müller, Norbert | - |
dc.contributor.nonIdAuthor | Neumann, Eike | - |
dc.contributor.nonIdAuthor | Preining, Norbert | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.