On the completeness of the inductive assertion method

DOI10.1016/S0022-0000(75)80056-0zbMath0353.68040OpenAlexW2113090411MaRDI QIDQ1236426

L. G. L. T. Meertens, J. W. de Bakker

Publication date: 1975

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0022-0000(75)80056-0

Mathematics Subject Classification ID

General topics in the theory of software (68N01)

Related Items

Developments in concurrent Kleene algebra ⋮ Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming ⋮ Natural Quantum Operational Semantics with Predicates ⋮ Exploring an Interface Model for CKA ⋮ Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic ⋮ Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. I ⋮ The Birth of Model Checking ⋮ Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II ⋮ Axiomatic data type specifications: A first order theory of linear lists ⋮ Semantical analysis of specification logic ⋮ Programs as partial graphs. I: Flow equivalence and correctness ⋮ Programs as partial graphs. II: Recursion ⋮ An execution mechanism for nondeterministic, state-oriented programs based on a chart parser ⋮ Least fixed points revisited ⋮ Generalised quantum weakest preconditions ⋮ Recursive assertions are not enough - or are they? ⋮ Propositional dynamic logic of nonregular programs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mathematical theory of partial correctness
• Decidable Properties of Monadic Functional Schemas
• Inductive methods for proving properties of programs
• An axiomatic basis for computer programming
• Formalization of Properties of Functional Programs
• Fixpoint approach to the theory of computation