Saved in:
| Main Authors: | , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2016
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/1608.05787 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914901068349440 |
|---|---|
| author | Park, Sewon Brauße, Franz Collins, Pieter Kim, SunYoung Konečný, Michal Lee, Gyesik Müller, Norbert Neumann, Eike Preining, Norbert Ziegler, Martin |
| author_facet | Park, Sewon Brauße, Franz Collins, Pieter Kim, SunYoung Konečný, Michal Lee, Gyesik Müller, Norbert Neumann, Eike Preining, Norbert Ziegler, Martin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1608_05787 |
| institution | arXiv |
| publishDate | 2016 |
| record_format | arxiv |
| spellingShingle | Semantics, Specification Logic, and Hoare Logic of Exact Real Computation Park, Sewon Brauße, Franz Collins, Pieter Kim, SunYoung Konečný, Michal Lee, Gyesik Müller, Norbert Neumann, Eike Preining, Norbert Ziegler, Martin Numerical Analysis Logic in Computer Science 03B70, 65Y99, 68P, 68N, 68Q F.3.1; G.1.0; I.1.2 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. |
| title | Semantics, Specification Logic, and Hoare Logic of Exact Real Computation |
| topic | Numerical Analysis Logic in Computer Science 03B70, 65Y99, 68P, 68N, 68Q F.3.1; G.1.0; I.1.2 |
| url | https://arxiv.org/abs/1608.05787 |