On the completeness of the inductive assertion method

DOI10.1016/S0022-0000(75)80056-0MaRDI QIDQ1236426zbMATH OpenOpenAlexFDO

Authors 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)

Cites work

• An axiomatic basis for computer programming
• Decidable Properties of Monadic Functional Schemas
• Fixpoint approach to the theory of computation
• Formalization of Properties of Functional Programs
• scientific article; zbMATH DE number 3602653 (Why is no real title available?)
• scientific article; zbMATH DE number 3448070 (Why is no real title available?)
• scientific article; zbMATH DE number 3430635 (Why is no real title available?)
• scientific article; zbMATH DE number 3293666 (Why is no real title available?)
• scientific article; zbMATH DE number 3302923 (Why is no real title available?)
• scientific article; zbMATH DE number 3410596 (Why is no real title available?)
• scientific article; zbMATH DE number 3413799 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Inductive methods for proving properties of programs
• Mathematical theory of partial correctness

Cited in

(17)

• Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic
• Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. I
• Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II
• Axiomatic data type specifications: A first order theory of linear lists
• 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
• Recursive assertions are not enough - or are they?
• Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming
• Exploring an interface model for CKA
• Developments in concurrent Kleene algebra
• The Birth of Model Checking
• Natural Quantum Operational Semantics with Predicates
• Propositional dynamic logic of nonregular programs
• Semantical analysis of specification logic
• Generalised quantum weakest preconditions

This page was built for publication: On the completeness of the inductive assertion method

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