TY - BOOK ID - 5292609 TI - Modular Specification and Verification of Object-Oriented Programs PY - 2002 VL - 2262 SN - 03029743 SN - 3540431675 9783540431671 3540456511 PB - Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, DB - UniCat KW - Object-oriented programming (Computer science) KW - Modular programming KW - Computer software KW - Programmation orientée objet (Informatique) KW - Logiciels KW - Development KW - Développement KW - Computer Science KW - Engineering & Applied Sciences KW - Modular programming. KW - Development. KW - Programmation orientée objet (Informatique) KW - Développement KW - Development of computer software KW - Software development KW - Computer science. KW - Software engineering. KW - Computer programming. KW - Programming languages (Electronic computers). KW - Computer logic. KW - Computer Science. KW - Programming Techniques. KW - Programming Languages, Compilers, Interpreters. KW - Software Engineering/Programming and Operating Systems. KW - Software Engineering. KW - Logics and Meanings of Programs. KW - Computer programming KW - Object-oriented methods (Computer science) KW - Document Object Model (Web site development technology) KW - Logic design. KW - Design, Logic KW - Design of logic systems KW - Digital electronics KW - Electronic circuit design KW - Logic circuits KW - Machine theory KW - Switching theory KW - Computer software engineering KW - Engineering KW - Informatics KW - Science KW - Computer languages KW - Computer program languages KW - Computer programming languages KW - Machine language KW - Electronic data processing KW - Languages, Artificial KW - Computers KW - Electronic computer programming KW - Electronic digital computers KW - Programming (Electronic computers) KW - Coding theory KW - Computer science logic KW - Logic, Symbolic and mathematical KW - Programming KW - Computer software - Development KW - Programming languages (Electronic computers) UR - https://www.unicat.be/uniCat?func=search&query=sysid:5292609 AB - Software systems play an increasingly important role in modern societies. Smart cards for personal identi?cation, e-banking, software-controlled me- cal tools, airbags in cars, and autopilots for aircraft control are only some examples that illustrate how everyday life depends on the good behavior of software. Consequently, techniques and methods for the development of hi- quality, dependable software systems are a central research topic in computer science. A fundamental approach to this area is to use formal speci?cation and veri?cation. Speci?cation languages allow one to describe the crucial p- perties of software systems in an abstract, mathematically precise, and implementation-independent way. By formal veri?cation, one can then prove that an implementation really has the desired, speci?ed properties. Although this formal methods approach has been a research topic for more than 30 years, its practical success is still restricted to domains in which devel- ment costs are of minor importance. Two aspects are crucial to widen the application area of formal methods: – Formal speci?cation techniques have to be smoothly integrated into the software and program development process. – The techniques have to be applicable to reusable software components. This way, the quality gain can be exploited for more than one system, thereby justifying the higher development costs. Starting from these considerations, Peter Muller ¨ has developed new te- niques for the formal speci?cation and veri?cation of object-oriented so- ware. The speci?cation techniques are declarative and implementati- independent. They can be used for object-oriented design and programming. ER -