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 predicates. Various examples demonstrate the practicality and convenience of our language and proof rules.

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