On the notion of expressiveness and the rule of adaptation

DOI10.1016/0304-3975(83)90009-9zbMath0511.68006OpenAlexW2068567986MaRDI QIDQ1838825

Ernst-Ruediger Olderog

Publication date: 1983

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

Full work available at URL: https://doi.org/10.1016/0304-3975(83)90009-9

zbMATH Keywords

expressivenessassertion languagecompleteness of Hoare-like proof systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items (11)

Being and Change: Reasoning About Invariance ⋮ A sharp proof rule for procedures in WP semantics ⋮ Some general incompleteness results for partial correctness logics ⋮ On the completeness of modular proof systems ⋮ Fifty years of Hoare's logic ⋮ Hoare's logic and VDM ⋮ Wythoff games, continued fractions, cedar trees and Fibonacci searches ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach ⋮ A proof outline logic for object-oriented programming ⋮ Correctness of programs with Pascal-like procedures without global variables ⋮ Some questions about expressiveness and relative completeness in Hoare's logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Expressiveness and the completeness of Hoare's logic
• The logic of aliasing
• Sound and complete Hoare-like calculi based on copy rules
• A simple relation between relational and predicate transformer semantics for nondeterministic programs
• Proof rules for the programming language Euclid
• Completeness with Finite Systems of Intermediate Assertions for Recursive Program Schemes
• Assignment and Procedure Call Proof Rules
• Ten Years of Hoare's Logic: A Survey—Part I
• Generic commands--a tool for partial correctness formalisms
• Soundness and Completeness of an Axiom System for Program Verification
• Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
• Programming as a Discipline of Mathematical Nature
• An axiomatic basis for computer programming

This page was built for publication: On the notion of expressiveness and the rule of adaptation