Definition and basic properties of the Deva meta-calculus (Q688825)

The current situation with respect to the application of formal software development methods is characterized by a partial utilization of the benefits offered by the formal approach to software development: more and more systems are successfully specified in formal notations, however formal developments down to efficient implementations and inclusive of all necessary proofs are still very rare. The formal specification of software systems has been relatively successful because it helps yield precise knowledge and understanding of the problem to be solved: information which will effect significant benefits in the subsequent development phase. The formal development of software systems, in the above sense, has been much less successful because with growing size of examples, the transitions and proofs quickly become too complex to be effectively understood and managed, regardless of the degree of automatic support. The enormous amount of necessary proofs, which are mostly of technical nature, is, in the author's view, not inherent to the software development process as such, but is due to a lack of well designed and generally accepted methods and notation, a lack of a library of generally accepted standard theories for software development, and a lack of tools which support all this. On the other hand, theoretical research has produced remarkable progress towards the development and investigation of powerful generic proof frameworks, based on typed \(\lambda\)-calulus, that offer a natural and universal formal derivation machinery and can be instantiated by various logical and mathematical theories. Most of these frameworks have been designed and used within a theoretical environment, to study issues of formalization and proof. The article reports on the definition and theoretical investigation of a generic development framework designed to express completely formal developments. This framework, named Deva meta-calculus, can be seen as a contribution towards linking work performed on proof frameworks with work on formal development methods. The connection consists of viewing developments as proofs and development methods as theories. As a result, development methods become complemently formalized objects. The purpose of Deva is to experiment with complete formalizations of currently known methods and with the resulting method support systems. This experimentation can be a quite rewarding process, e.g. by pointing out informal parts both in the method itself and in its use. Similarly, it is interesting to experiment with libraries of basic theories for software developments based on the method.