Floyd's principle, correctness theories and program equivalence

DOI10.1016/0304-3975(82)90001-9zbMath0474.68017OpenAlexW2140892158MaRDI QIDQ1158948

Jerzy Tiuryn, J. V. Tucker, Jan A. Bergstra

Publication date: 1982

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

Full work available at URL: https://dspace.library.uu.nl/handle/1874/12712

zbMATH Keywords

algebraic specificationsprogramming systemsarithmetical computationdata abstractionsdeterministic control and assignment constructsfirst-order assertionsfirst-order specification language

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (9)

Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs ⋮ Determinateness of program equivalence over peano axioms ⋮ Hoare's logic and Peano's arithmetic ⋮ European Summer Meeting of the Association for Symbolic Logic, Paris, 1985 ⋮ Proving program inclusion using Hoare's logic ⋮ Two theorems about the completeness of Hoare's logic ⋮ Average case optimality for linear problems ⋮ Expressiveness and the completeness of Hoare's logic ⋮ The axiomatic semantics of programs based on Hoare's logic

Uses Software

• ALGOL 68

Cites Work

• Final algebra semantics and data type extensions
• A proof system for the first-order relational calculus
• Theory of program structures: Schemes, semantics, verification
• First-order dynamic logic
• Model theory
• An axiomatic definition of the programming language Pascal
• Consistent and complementary formal theories of the semantics of programming languages
• Soundness and Completeness of an Axiom System for Program Verification
• Programming as a Discipline of Mathematical Nature
• An axiomatic basis for computer programming
• Abstract First Order Computability. I
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Floyd's principle, correctness theories and program equivalence