A relation algebraic model of robust correctness

DOI10.1016/0304-3975(96)88664-6MaRDI QIDQ1350502zbMATH OpenOpenAlexFDO

Authors Thomas F. Gritzner, Rudolf Berghammer

Publication date 27 February 1997

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(96)88664-6

zbMATH Keywords

weakest preconditionsdemonic nondeterminismspecification statementrelational specificationrobust correct refinementsemantics of specifications and programs

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Relational mathematics for relative correctness
• Relational semantics of linear logic and higher-order model checking
• Algebraic models of correctness for microprocessors
• Relational algebraic semantics of deterministic and nondeterministic programs
• A machine-checked framework for relational separation logic
• Modal Kleene algebra applied to program correctness
• General correctness algebra
• Correctness criteria for algebraic closures of the estimate-calculating algorithm model
• scientific article; zbMATH DE number 67020

Cites work

• scientific article; zbMATH DE number 4020448 (Why is no real title available?)
• scientific article; zbMATH DE number 46424 (Why is no real title available?)
• scientific article; zbMATH DE number 46740 (Why is no real title available?)
• scientific article; zbMATH DE number 475192 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• scientific article; zbMATH DE number 970745 (Why is no real title available?)
• scientific article; zbMATH DE number 3070503 (Why is no real title available?)
• A RELATIONAL MODEL OF DEMONIC NONDETERMINISTIC PROGRAMS
• A Transformation System for Developing Recursive Programs
• A theoretical basis for stepwise refinement and the programming calculus
• Boolean Algebras with Operators
• Countable nondeterminism and random assignment
• Embedding a demonic semilattice in a relation algebra
• Laws of programming
• Predicative programming Part I
• Relation algebras: Concept of points and representability
• The specification statement

Cited in

(9)

• Fixpoints for general correctness
• Embedding a demonic semilattice in a relation algebra
• Relational mathematics for relative correctness
• Imperative abstractions for functional actions
• Relational semantics revisited
• Correctness criteria for algebraic closures of the estimate-calculating algorithm model
• Unifying lazy and strict computations
• A RELATIONAL MODEL OF DEMONIC NONDETERMINISTIC PROGRAMS
• An Analysis of Total Correctness Refinement Models for Partial Relation Semantics II

This page was built for publication: A relation algebraic model of robust correctness

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