scientific article; zbMATH DE number 18650

DOI10.1007/3-540-53487-3_39MaRDI QIDQ3976056zbMATH OpenFDO

Authors Christopher P. Lewington

Publication date 26 June 1992

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-53487-3_39

zbMATH Keywords

constructive theoriesformal specification methodssoftware development

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

[For the entire collection see Zbl 0731.00025.] The author thinks that constructive methodologies and formal specification methods (e.g. VDM), which are considered to be alternative approaches to software development in current opinion, may have much often one another. This paper is devoted to this envisagement. The author interprets a simple VDM operation specification into the constructive theory TK and provides a proof of the interpreted specification one may obtain via realizability of a program which meets the TK specification. He provides a `transformation package', consisting of a language interpretation, an eureka definition and some correctness-preserving transformation rules. Although the work is preliminary, it has provided an initial insight into the way in which constructive theories and formal methods may interact to yield a more satisfactory approach to software specification and development.

Recommendations

• scientific article; zbMATH DE number 3936465
• scientific article; zbMATH DE number 4016178
• Constructive programming: A personal view
• scientific article; zbMATH DE number 550761
• scientific article; zbMATH DE number 683356

Cited in

(2)

• Constructive programming: A personal view
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control

This page was built for publication:

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