An elementary and unified approach to program correctness

DOI10.1007/S00165-009-0137-4MaRDI QIDQ607408zbMATH OpenOpenAlexFDO

Authors Jaime A. Bohórquez V.

Publication date 22 November 2010

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-009-0137-4

zbMATH Keywords

recursionprogram verificationprogram correctnessprogramming methodologyDijkstra-Hehner language

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Dijkstra-Scholten predicate calculus: Concepts and misconceptions
• Partial correctness: The term-wise approach
• Laws of programming
• A theoretical basis for stepwise refinement and the programming calculus
• Dijkstra's interpretation of the approach to solving a problem of program correctness

Cites work

• scientific article; zbMATH DE number 3686772 (Why is no real title available?)
• scientific article; zbMATH DE number 3705887 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3787987 (Why is no real title available?)
• scientific article; zbMATH DE number 46740 (Why is no real title available?)
• scientific article; zbMATH DE number 3550181 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 517330 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 970745 (Why is no real title available?)
• A practical theory of programming
• A presentation of the Fibonacci algorithm
• An Inductive Theorem on the Correctness of General Recursive Programs
• An axiomatic basis for computer programming
• Exercises in Quantifier Manipulation
• Guarded commands, nondeterminacy and formal derivation of programs
• Intuitionistic logic according to Dijkstra's calculus of equational deduction
• On calculational proofs
• On the shape of mathematical arguments
• Predicative programming Part I
• Program development by stepwise refinement
• Programs are predicates
• Retrospective and Prospective for Unifying Theories of Programming
• The associativity of equivalence and the Towers of Hanoi problem
• The derivation of systolic computations
• The weakest prespecification

Cited in

(8)

• Unifying Recursion in Partial, Total and General Correctness
• Program correctness and matricial iteration theories
• Dijkstra's interpretation of the approach to solving a problem of program correctness
• General correctness: A unification of partial and total correctness
• scientific article; zbMATH DE number 5199012 (Why is no real title available?)
• The Formal System of Dijkstra and Scholten
• Loop verification with invariants and contracts
• Correctness of programs with Pascal-like procedures without global variables

Describes a project that uses

Uses Software

• CalcCheck

This page was built for publication: An elementary and unified approach to program correctness

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