No label defined (Q3976056)

[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.