An elementary and unified approach to program correctness

DOI10.1007/s00165-009-0137-4zbMath1211.68079OpenAlexW2017923582MaRDI QIDQ607408

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)

Related Items

Loop verification with invariants and contracts ⋮ The Formal System of Dijkstra and Scholten

Uses Software

• CalcCheck

Cites Work

• A practical theory of programming
• The derivation of systolic computations
• Intuitionistic logic according to Dijkstra's calculus of equational deduction
• A presentation of the Fibonacci algorithm
• The weakest prespecification
• On the shape of mathematical arguments
• The associativity of equivalence and the Towers of Hanoi problem
• Programs are predicates
• Exercises in Quantifier Manipulation
• Predicative programming Part I
• Guarded commands, nondeterminacy and formal derivation of programs
• Retrospective and Prospective for Unifying Theories of Programming
• An Inductive Theorem on the Correctness of General Recursive Programs
• An axiomatic basis for computer programming
• Program development by stepwise refinement
• On calculational proofs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item