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

TL;DR

This paper introduces ERC, a formal programming language for exact real number computation with a denotational semantics, and extends Hoare logic for verifying correctness of programs involving real numbers.

Contribution

It presents ERC, a new language with a formal semantics for exact real computation, and develops an extended Hoare logic for program correctness verification.

Findings

ERC captures all computable real functions

The logic for specifications is decidable and model-complete

Examples demonstrate practical applicability of the language and logic

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.