Hierarchical program specification and verification - a many-sorted logical approach

DOI10.1007/BF00288541zbMath0432.68011MaRDI QIDQ1138904

Reiji Nakajima, Hayao Nakahara, Michio Honda

Publication date: 1980

Published in: Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

verificationspecificationfirst order logicmany-sorted logichierarchical program specificationvalidation of implementations

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)

Related Items

Modularization and abstraction in logic programming, Lax naturality through enrichment, Specifications, models, and implementations of data abstractions, Formal system of definition of data sets as a high-level tool of data extraction, Semantics of algorithmic languages

Cites Work

• Remarks on 'Program proving: Jumps and functions' by M. Clint and C.A.R. Hoare
• Axioms for total correctness
• Program proving: KJumps and functions
• Proof of correctness of data representations
• Abstraction mechanisms in CLU
• Abstract data types and software validation
• Unnamed Item
• Unnamed Item