Semantical proofs of correctness for programs performing non-deterministic tests on real numbers

DOI10.1017/S0960129510000186MaRDI QIDQ3060187zbMATH OpenFDO

Authors Thomas Anberrée

Publication date 1 December 2010

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

denotational semanticsSmyth power domains

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• A Denotational Semantics for Total Correctness of Sequential Exact Real Programs
• scientific article; zbMATH DE number 4006264
• scientific article; zbMATH DE number 1760049
• Total correctness in nonstandard logics of programs
• scientific article; zbMATH DE number 3936484
• Verification, Model Checking, and Abstract Interpretation
• Partiality and nondeterminacy in program proofs
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• scientific article; zbMATH DE number 4005583

Cites work

• Domain-Theoretic Foundations of Functional Programming
• LCF considered as a programming language
• Recursive characterization of computable real-valued functions and relations
• Semantics of a sequential language for exact real-number computation

Cited in

(4)

• Computable decision making on the reals and other spaces. Via partiality and nondeterminism
• A Denotational Semantics for Total Correctness of Sequential Exact Real Programs
• Semantics of a sequential language for exact real-number computation
• Validating Brouwer's continuity principle for numbers using named exceptions

This page was built for publication: Semantical proofs of correctness for programs performing non-deterministic tests on real numbers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3060187)