The generic development language. Presentation and case studies (Q690318)

Formal specification methods gain in importance as tools are available supporting the specifier; in recent years, theoretical computer science has developed a lot of mechanisms that can be implemented on today's hardware efficiently. Therefore, it is not surprising that books presenting tools for reasoning about different phases of software engineering appear one after the other. The Deva approach emphasizes formal reasoning about program development, since more proofs are required during this phase than during the specification phase. A key concept of the Deva approach is viewing proofs as formal objects relating specifications to programs. They correspond to functions in a higher-order typed \(\lambda\)-calculus. Since the propositions correspond to types, putting partial proofs together becomes a type-checking problem. For structuring proofs in the large, the Deva language supports the concept of parameterized modules and inheritance. The authors claim that Deva is not restricted to a specific development method, but allows various methods. The book comprises five major chapters. After a brief introduction, chapter 2 gives a survey of Deva by presenting intuitive examples from elementary mathematics and logic. This chapter shows how to use the language, whereas the next chapter is concerned with its formal definition. It first presents a sublanguage, the kernel, which introduces all essential semantic relations, and then discusses the remaining operations. This explicit part of Deva, however, forces the user to consider too much detail. Therefore, an implicit part introduces some simplifications, e.g. the use of special contexts. Chapters 4-6 demonstrate the power of Deva. First, some well-known basic theories used later on in the case studies, are formalized as Deva contexts. We find, e.g., the Deva notations for propositional and predicate logic, finite sets, sequences, and extensional equality of terms. The first case study (chapter 5) is an application of Deva to VDM- style development. It shows how to formally reason about VDM. First reification in VDM is described in Deva notation; then, an example taken from biology (the human leucocyte antigen typing problem) is completely formalized. The last section of this chapter proves that VDM specification is transitive. Finally, the second case study (chapter 6) treats another algorithmic calculus for developing programs from specification (the Bird-Meertens Formalism). An interesting example in this chapter shows how the \(\alpha\beta\)-pruning strategy for two-player game trees can be derived from the minimax evaluation scheme. Overall, this book gives a correct impression of what is possible in formalized program development today.