Towards constructive program derivation in VDM

Abstract

Formal specification methods and constructive theories are generally considered to be alternative approaches to software development. In this paper we demonstrate that the two paradigms in fact have much to offer one another. The shortcomings of the two approaches include inadequate program derivation techniques for formal methods and poor specification facilities in constructive theories. Here we examine how the program extraction power of the constructive theory TK may be coupled with simple specifications written in VDM to suggest the possibility of a more coherent approach to software development.