No Cover Image

Journal article 139 views 12 downloads

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

Logical Methods in Computer Science, Volume: 20, Issue: 2

Swansea University Author: Eike Neumann Orcid Logo

  • 69244.VoR.pdf

    PDF | Version of Record

    Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license.

    Download (732.16KB)

Check full text

DOI (Published version): 10.46298/lmcs-20(2:17)2024

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

Full description

Published in: Logical Methods in Computer Science
ISSN: 1860-5974
Published: Centre pour la Communication Scientifique Directe (CCSD) 2024
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa69244
first_indexed 2025-04-09T12:39:05Z
last_indexed 2025-05-20T06:51:15Z
id cronfa69244
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2025-05-19T14:14:03.8383750</datestamp><bib-version>v2</bib-version><id>69244</id><entry>2025-04-09</entry><title>Semantics, Specification Logic, and Hoare Logic of Exact Real Computation</title><swanseaauthors><author><sid>1bf535eaa8d6fcdfbd464a511c1c0c78</sid><ORCID>0009-0003-2907-1566</ORCID><firstname>Eike</firstname><surname>Neumann</surname><name>Eike Neumann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2025-04-09</date><deptcode>MACS</deptcode><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 Z&#x220B;p&#x21A6;2p&#x2208;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.</abstract><type>Journal Article</type><journal>Logical Methods in Computer Science</journal><volume>20</volume><journalNumber>2</journalNumber><paginationStart/><paginationEnd/><publisher>Centre pour la Communication Scientifique Directe (CCSD)</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic>1860-5974</issnElectronic><keywords>Mathematics - Numerical Analysis,Computer Science - Logic in Computer Science,03B70, 65Y99, 68P, 68N, 68Q,F.3.1,G.1.0,I.1.2</keywords><publishedDay>24</publishedDay><publishedMonth>6</publishedMonth><publishedYear>2024</publishedYear><publishedDate>2024-06-24</publishedDate><doi>10.46298/lmcs-20(2:17)2024</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders>This work was supported by the National Research Foundation of Korea (grants NRF2017R1E1A1A03071032 and NRF-2017R1D1A1B05031658), by the International Research &amp; Development Program of the Korean Ministry of Science and ICT (grant NRF-2016K1A3A7A03950702), by the European Union&#x2019;s Horizon 2020 research and innovation program under the Marie Sklodowska-Curie grant agreement No 731143, and by the German Research Foundation (DFG) Grant MU 1801/5-1.</funders><projectreference/><lastEdited>2025-05-19T14:14:03.8383750</lastEdited><Created>2025-04-09T13:35:11.4087039</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Sewon</firstname><surname>Park</surname><order>1</order></author><author><firstname>Franz</firstname><surname>Brau&#xDF;e</surname><order>2</order></author><author><firstname>Pieter</firstname><surname>Collins</surname><order>3</order></author><author><firstname>SunYoung</firstname><surname>Kim</surname><order>4</order></author><author><firstname>Michal</firstname><surname>Kone&#x10D;n&#xFD;</surname><order>5</order></author><author><firstname>Gyesik</firstname><surname>Lee</surname><order>6</order></author><author><firstname>Norbert</firstname><surname>M&#xFC;ller</surname><order>7</order></author><author><firstname>Eike</firstname><surname>Neumann</surname><orcid>0009-0003-2907-1566</orcid><order>8</order></author><author><firstname>Norbert</firstname><surname>Preining</surname><order>9</order></author><author><firstname>Martin</firstname><surname>Ziegler</surname><order>10</order></author></authors><documents><document><filename>69244__34148__088098ced37c4af3922d8ab35f6a4c19.pdf</filename><originalFilename>69244.VoR.pdf</originalFilename><uploaded>2025-04-30T14:45:26.4032720</uploaded><type>Output</type><contentLength>749729</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0</licence></document></documents><OutputDurs/></rfc1807>
spelling 2025-05-19T14:14:03.8383750 v2 69244 2025-04-09 Semantics, Specification Logic, and Hoare Logic of Exact Real Computation 1bf535eaa8d6fcdfbd464a511c1c0c78 0009-0003-2907-1566 Eike Neumann Eike Neumann true false 2025-04-09 MACS 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 Z∋p↦2p∈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. Journal Article Logical Methods in Computer Science 20 2 Centre pour la Communication Scientifique Directe (CCSD) 1860-5974 Mathematics - Numerical Analysis,Computer Science - Logic in Computer Science,03B70, 65Y99, 68P, 68N, 68Q,F.3.1,G.1.0,I.1.2 24 6 2024 2024-06-24 10.46298/lmcs-20(2:17)2024 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University This work was supported by the National Research Foundation of Korea (grants NRF2017R1E1A1A03071032 and NRF-2017R1D1A1B05031658), by the International Research & Development Program of the Korean Ministry of Science and ICT (grant NRF-2016K1A3A7A03950702), by the European Union’s Horizon 2020 research and innovation program under the Marie Sklodowska-Curie grant agreement No 731143, and by the German Research Foundation (DFG) Grant MU 1801/5-1. 2025-05-19T14:14:03.8383750 2025-04-09T13:35:11.4087039 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Sewon Park 1 Franz Brauße 2 Pieter Collins 3 SunYoung Kim 4 Michal Konečný 5 Gyesik Lee 6 Norbert Müller 7 Eike Neumann 0009-0003-2907-1566 8 Norbert Preining 9 Martin Ziegler 10 69244__34148__088098ced37c4af3922d8ab35f6a4c19.pdf 69244.VoR.pdf 2025-04-30T14:45:26.4032720 Output 749729 application/pdf Version of Record true Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license. true eng https://creativecommons.org/licenses/by/4.0
title Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
spellingShingle Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
Eike Neumann
title_short Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
title_full Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
title_fullStr Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
title_full_unstemmed Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
title_sort Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
author_id_str_mv 1bf535eaa8d6fcdfbd464a511c1c0c78
author_id_fullname_str_mv 1bf535eaa8d6fcdfbd464a511c1c0c78_***_Eike Neumann
author Eike Neumann
author2 Sewon Park
Franz Brauße
Pieter Collins
SunYoung Kim
Michal Konečný
Gyesik Lee
Norbert Müller
Eike Neumann
Norbert Preining
Martin Ziegler
format Journal article
container_title Logical Methods in Computer Science
container_volume 20
container_issue 2
publishDate 2024
institution Swansea University
issn 1860-5974
doi_str_mv 10.46298/lmcs-20(2:17)2024
publisher Centre pour la Communication Scientifique Directe (CCSD)
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description 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 Z∋p↦2p∈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.
published_date 2024-06-24T05:40:32Z
_version_ 1835602786471903232
score 11.064671

Similar Items