Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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, Norbert Preining, Martin Ziegler

TL;DR

This work introduces ERC, an imperative language for exact real computation with Kleenean three-valued logic and a computable Plotkin powerdomain denotational semantics that faithfully capture multi-valued nondeterminism. ERC supports exact real arithmetic, limit behavior via precision parameters, and a decidable base theory for reasoning about specifications, while extending Hoare logic to total correctness in this setting. It establishes Turing-completeness over integers, showing ERC can realize all computable partial real and integer multi-valued functions, and demonstrates practical verification through root-finding and other numerical routines. The framework enables provably correct exact numerical computations with a rigorous, decidable specification language, offering a principled path toward reliable exact-real software engineering.

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 $\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.

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

TL;DR

This work introduces ERC, an imperative language for exact real computation with Kleenean three-valued logic and a computable Plotkin powerdomain denotational semantics that faithfully capture multi-valued nondeterminism. ERC supports exact real arithmetic, limit behavior via precision parameters, and a decidable base theory for reasoning about specifications, while extending Hoare logic to total correctness in this setting. It establishes Turing-completeness over integers, showing ERC can realize all computable partial real and integer multi-valued functions, and demonstrates practical verification through root-finding and other numerical routines. The framework enables provably correct exact numerical computations with a rigorous, decidable specification language, offering a principled path toward reliable exact-real software engineering.

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

Paper Structure

This paper contains 43 sections, 13 theorems, 92 equations, 3 figures, 10 algorithms.

Table of Contents

  1. Introduction
  2. Related Works
  3. Kleenean-valued Comparison and Nondeterminism
  4. Main Contributions and Overviews
  5. Preliminaries
  6. Representations and Computable Partial Functions
  7. Computable Infinite Multi-valued functions
  8. Computable (Finite) Multi-valued functions and Plotkin Powerdomain
  9. Formal Syntax and Typing Rules of Exact Real Computation
  10. Syntax
  11. Data Types
  12. Terms
  13. Commands
  14. Programs
  15. Typing Rules
  16. ...and 28 more sections

Key Result

Lemma 3.2

Whenever $\Gamma \vdash S \triangleright \Gamma'$, the new context $\Gamma'$ is an extension of $\Gamma$ in the sense that there is a context $\Delta$ such that $\Gamma' = \Gamma, \Delta$.

Figures (3)

  • Figure 1: Typing rules for terms
  • Figure 2: Typing rules for commands
  • Figure 3: The Hoare logic of $\textup{ERC}\xspace(\mathcal{F}, \mathcal{G})$

Theorems & Definitions (42)

  • Remark 1.1
  • Remark 2.5
  • Remark 2.6
  • Lemma 3.2
  • Definition 4.1
  • Definition 4.2
  • Lemma 4.3
  • Definition 4.4
  • Proposition 4.5
  • proof
  • ...and 32 more