Sewon Park ; Franz Brauße ; Pieter Collins ; SunYoung Kim ; Michal Konečný et al. - Semantics, Specification Logic, and Hoare Logic of Exact Real Computation

lmcs:7557 - Logical Methods in Computer Science, June 24, 2024, Volume 20, Issue 2 - https://doi.org/10.46298/lmcs-20(2:17)2024
Semantics, Specification Logic, and Hoare Logic of Exact Real ComputationArticle

Authors: Sewon Park ; Franz Brauße ; Pieter Collins ; SunYoung Kim ; Michal Konečný ; Gyesik Lee ; Norbert Müller ; Eike Neumann ; Norbert Preining ; Martin Ziegler

    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.


    Volume: Volume 20, Issue 2
    Published on: June 24, 2024
    Accepted on: May 4, 2024
    Submitted on: June 8, 2021
    Keywords: Mathematics - Numerical Analysis,Computer Science - Logic in Computer Science,03B70, 65Y99, 68P, 68N, 68Q,F.3.1,G.1.0,I.1.2

    Consultation statistics

    This page has been seen 250 times.
    This article's PDF has been downloaded 100 times.