English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We propose a simple imperative programming language, ERC, that featuresarbitrary real numbers as primitive data type, exactly. Equipped with adenotational semantics, ERC provides a formal programming language-theoreticfoundation to the algorithmic processing of real numbers. In order to capturemulti-valuedness, which is well-known essential to real number computation, weuse a carefully designed Plotkin powerdomain. This makes our programminglanguage semantics computable and complete: all and only real functionscomputable in computable analysis can be realized in ERC. The base programminglanguage supports real arithmetic as well as implicit limits; expansionssupport additional primitive operations (such as a user-defined exponentialfunction). By restricting integers to Presburger arithmetic and real coercionto the `precision' embedding $Z\ni p\mapsto 2^p\in R$, we arrive at afirst-order theory which we prove to be decidable, model-complete, andexpressive for the base programming language. Based on said logic asspecification language for preconditions and postconditions, we extend Hoarelogic to a sound (w.r.t. the denotational semantics) and expressive system forderiving correct TOTAL correctness predicates. Various examples demonstrate thepracticality and convenience of our language and proof rules.

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