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

DOI10.1007/BF00288541MaRDI QIDQ1138904zbMATH OpenFDO

Authors Reiji Nakajima, Michio Honda, Hayao Nakahara

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

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

Cites work

• scientific article; zbMATH DE number 3566134 (Why is no real title available?)
• scientific article; zbMATH DE number 3248792 (Why is no real title available?)
• Abstract data types and software validation
• Abstraction mechanisms in CLU
• Axioms for total correctness
• Program proving: KJumps and functions
• Proof of correctness of data representations
• Remarks on 'Program proving: Jumps and functions' by M. Clint and C.A.R. Hoare

Cited in

(5)

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

This page was built for publication: Hierarchical program specification and verification - a many-sorted logical approach

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