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.

翻译：我们提出一种简单的命令式编程语言ERC，该语言以任意实数作为原始数据类型，并实现精确计算。通过配备指称语义，ERC为实数的算法处理提供了形式化的编程语言理论基础。为捕捉多值性（这已被证明是实数计算的核心要素），我们采用Plotkin幂域结构，使编程语言语义具有可计算性和完备性：所有且仅有的可计算分析中的可计算实数函数均可在ERC中实现。基础编程语言支持实数算术与隐式极限运算，扩展机制支持附加原语操作（如用户自定义指数函数）。通过将整数限制为Presburger算术，并将实数强制转换约束为精度嵌入$\mathbb{Z}\ni p\mapsto 2^p\in\mathbb{R}$，我们获得了一个可判定且模型完备的一阶理论。基于该逻辑作为前置条件与后置条件的规约语言，我们将霍尔逻辑扩展为（相对于指称语义）可靠且充分表达的系统，用于推导正确的完全正确性规约。多个示例展示了本语言及扩展霍尔逻辑的实用性与便捷性。