No Cover Image

Journal article 57 views

Semantics, Specification Logic, and Hoare Logic of Exact Real Computation

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

Logical Methods in Computer Science, Volume: 20, Issue: 2

Swansea University Author: Eike Neumann Orcid Logo

  • 69244.VoR.pdf

    PDF | Version of Record

    Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license.

    Download (732.16KB)

Check full text

DOI (Published version): 10.46298/lmcs-20(2:17)2024

Abstract

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 m...

Full description

Published in: Logical Methods in Computer Science
ISSN: 1860-5974
Published: Centre pour la Communication Scientifique Directe (CCSD) 2024
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa69244
Abstract: 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 Z∋p↦2p∈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.
Keywords: Mathematics - Numerical Analysis,Computer Science - Logic in Computer Science,03B70, 65Y99, 68P, 68N, 68Q,F.3.1,G.1.0,I.1.2
College: Faculty of Science and Engineering
Funders: This work was supported by the National Research Foundation of Korea (grants NRF2017R1E1A1A03071032 and NRF-2017R1D1A1B05031658), by the International Research & Development Program of the Korean Ministry of Science and ICT (grant NRF-2016K1A3A7A03950702), by the European Union’s Horizon 2020 research and innovation program under the Marie Sklodowska-Curie grant agreement No 731143, and by the German Research Foundation (DFG) Grant MU 1801/5-1.
Issue: 2

Similar Items