Modular specification and verification of object-oriented programs
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 o...
Enregistré dans:
| 主要作者: | |
|---|---|
| 格式: | Livre numérique |
| 語言: | Anglais |
| 出版: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| 叢編: | Lecture notes in computer science
2262 |
| 主題: | |
| 在線閱讀: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| 提示: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Modular specification and verification of object-oriented programs, Peter Müller, Berlin, Springer, 2002, 1 vol. (XIV-292 p.), Lecture notes in computer science, 3-540-43167-5 • Modular Specification and Verification of Object-Oriented Programs, Texte imprimé, 9783662199466 |
| LEADER | 04367nam a22004217a 4500 | ||
|---|---|---|---|
| 001 | 949199 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155220748 | ||
| 020 | |a 9783540456513 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004 | ||
| 082 | |a 005.1 | ||
| 100 | 1 | |a Müller, Peter, |d 1961-...., |c informaticien. | |
| 245 | 1 | 0 | |a Modular specification and verification of object-oriented programs |c Peter Müller. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science |v 2262 |x 1611-3349 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a Mojave and the Universe Type System -- The Semantics of Mojave -- Modular Specification and Verification of Functional Behavior -- Modular Specification and Verification of Frame Properties -- Modular Specification and Verification of Type Invariants -- Conclusion -- Formal Background and Notations -- Predefined Type Declarations -- Examples -- Auxiliary Lemmas, Proofs, and Models. | |
| 506 | |a Accès en ligne pour les établissements français bénéficiaires des licences nationales | ||
| 506 | |a Accès soumis à abonnement pour tout autre établissement | ||
| 506 | |a Conditions particulières de réutilisation pour les bénéficiaires des licences nationales. https://www.licencesnationales.fr/springer-nature-ebooks-contrat-licence-ln-2017 | ||
| 520 | |a 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. | ||
| 650 | |a Génie logiciel | ||
| 650 | |a Informatique | ||
| 650 | |a Langages de programmation | ||
| 650 | |a Ordinateurs | ||
| 650 | |a Logiciels |x Développement | ||
| 650 | |a Programmation orientée objets (informatique) | ||
| 650 | |a Programmation modulaire | ||
| 776 | 0 | |0 069171653 |t Modular specification and verification of object-oriented programs |f Peter Müller |c Berlin |n Springer |d 2002 |p 1 vol. (XIV-292 p.) |s Lecture notes in computer science |z 3-540-43167-5 | |
| 776 | 0 | |t Modular Specification and Verification of Object-Oriented Programs |b Texte imprimé |z 9783662199466 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/3-540-45651-1 |z Accès sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-BGWM3JHC-1 |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:748056920 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-45651-1 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:751508268 |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-45651-1 |z Accès INSA CVL | |
| 997 | |0 949199 |1 Livre numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||