Modular specification and verification of object-oriented programs

>> Google Books

所蔵情報QRコード

Modular specification and verification of object-oriented programs / Peter Müller

資料種別:: 図書
出版情報:: Berlin : Springer, c2002
形態:: xiv, 292 p. ; 24 cm
シリーズ名:: Lecture notes in computer science ; 2262 <BA00009279>
著者名:: Müller, Peter
ISBN:: 9783540431671 [3540431675]
書誌ID:: BA55535248

子書誌情報

フルテキスト

所蔵情報

他の版・巻

書誌詳細

注記:

Bibliography: p. [271]-283
Includes index

主題:

Computer software--Development; Modular programming; Object-oriented programming (Computer science)

言語:

英語

目次情報:

Introduction / 1：

Motivation / 1.1：

Specification and Verification Technique / 1.2：

The Problem / 1.3：

Modular Correctness / 1.3.1：

The Frame Problem / 1.3.2：

Modular Verification of Type Invariants / 1.3.3：

The Extended State Problem / 1.3.4：

Alias Control / 1.3.5：

Modularity Aspects of Programs, Specifications, and Proofs / 1.4：

Modularity of Programs / 1.4.1：

Modularity of Universal Specifications / 1.4.2：

Modularity of Interface Specifications / 1.4.3：

Modularity of Correctness Proofs / 1.4.4：

Approach, Outline, and Contributions / 1.5：

Approach / 1.5.1：

Outline / 1.5.2：

Contributions / 1.5.3：

Related Work / 1.6：

Specification Techniques / 1.6.1：

Verification and Analysis Techniques / 1.6.2：

Mojave and the Universe Type System / 2：

Mojave: The Language / 2.1：

The Language Core / 2.1.1：

Modularity / 2.1.2：

Universes: A Type System for Flexible Alias Control / 2.2：

The Ownership Model / 2.2.1：

The Universe Programming Model / 2.2.2：

Programming with Universes / 2.2.3：

Examples / 2.2.4：

Formalization of the Universe Type System / 2.2.5：

Discussion / 2.2.6：

The Semantics of Mojave / 2.3：

Programming Logic / 3.1：

Formal Data and State Model / 3.1.1：

Axiomatic Semantics / 3.1.2：

Language Properties / 3.1.3：

Type Safety / 3.2.1：

Liveness Properties / 3.2.2：

Properties of Readonly Methods / 3.2.3：

Correctness / 3.3：

Correctness of Closed Programs / 3.3.1：

Correctness of Open Programs: Modular Correctness / 3.3.2：

Modular Soundness / 3.3.3：

Composition of Modular Correct Open Programs / 3.3.4：

Modular Specification and Verification of Functional Behavior / 3.4：

Foundations of Interface Specifications / 4.1：

Specification of Functional Behavior / 4.2：

Abstract Fields / 4.2.1：

Pre-post-specifications / 4.2.2：

Verification of Functional Behavior / 4.3：

Verification of Method Bodies / 4.3.1：

Proofs for Virtual Methods / 4.3.2：

Example / 4.3.3：

Modular Specification and Verification of Frame Properties / 4.4：

Meaning of Modifies-Clauses / 5.1：

Explicit Dependencies / 5.1.2：

Modularity Rules / 5.1.3：

Formalization of Explicit Dependencies / 5.2：

Declaration of Dependencies / 5.2.1：

Axiomatization of the Depends-Relation / 5.2.2：

Consistency with Representation / 5.2.3：

Formalization of the Modularity Rules / 5.2.4：

Axiomatization of the Notdepends-Relation / 5.2.5：

Formalization of Modifies-Clauses / 5.2.6：

Verification of Frame Properties / 5.4：

Local Update Property / 5.4.1：

Accessibility Properties / 5.4.3：

Modularity Theorem for Frame Properties / 5.4.4：

Leino's and Nelson's Work on Dependencies / 5.4.5：

Other Work on the Frame Problem / 5.5.2：

Modular Specification and Verification of Type Invariants / 6：

Motivation and Approach / 6.1：

Invariant Semantics for Nonmodular Programs / 6.1.1：

Problems for Modular Verification of Invariants / 6.1.2：

Specification of Type Invariants / 6.1.3：

Declaration of Type Invariants / 6.2.1：

Formal Meaning of Invariants / 6.2.2：

Verification of Type Invariants / 6.3：

Verification Methodology / 6.3.1：

Module Invariants / 6.3.2：

History Constraints / 6.4.2：

Conclusion / 6.5：

Summary and Contributions / 7.1：

The Lopex Project / 7.2：

Tool Support / 7.3：

Directions for Future Work / 7.4：

Formal Background and Notations / A：

Formal Background / A.1：

Notations / A.2：

Predefined Type Declarations / B：

Doubly Linked List / C：

Property Editor / C.2：

Auxiliary Lemmas, Proofs, and Models / D：

Auxiliary Lemmas and Proofs from Chapter 3 / D.1：

Auxiliary Lemmas and Proofs from Chapter 5 / D.2：

Auxiliary Lemmas and Proofs from Chapter 6 / D.3：

A Model for the Axiomatization of the Depends-Relation / D.4：

Bibliography

List of Figures

Index

Introduction / 1：

Motivation / 1.1：

Specification and Verification Technique / 1.2：

The Problem / 1.3：

Modular Correctness / 1.3.1：

The Frame Problem / 1.3.2：

続きを見る

東工大ブックレビュー

類似資料:

1 電子ブック Modular Specification and Verification of Object-Oriented Programs Müller, Peter SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg	7 図書 Research directions in object-oriented programming Shriver, Bruce D., 1940-, Wegner, Peter MIT Press
2 図書 Object-oriented software construction (: pbk) Meyer, Bertrand, 1950- Prentice-Hall	8 図書 Program development in Java : abstraction, specification, and object-oriented design (: alk. paper) Liskov, B., Guttag, John Addison-Wesley
3 図書 Object-oriented system development De Champeaux, Dennis, Lea, Douglas, Faure, Penelope Addison-Wesley	9 図書 Research directions in concurrent object-oriented programming Agha, Gul A., Wegner, Peter, 米沢, 明憲(1947-) MIT Press
4 図書 Readings in object-oriented systems and applications (: microfiche ; : paper ; : case) Rine, David C. IEEE Computer Society Press	10 図書 Object-oriented behavioral specifications Kilov, Haim, Harvey, William, 1938- Kluwer Academic Publishers
5 図書 Object-oriented environments : the Mjølner approach Knudsen, J. Lindskov Prentice Hall	11 図書 Formal specification and design Feijs, L. M. G. (Loe M. G.), Jonkers, H. B. M. Cambridge University Press
6 図書 Algebraic specification techniques in object oriented programming environments (: gw ; : us) Breu, R. (Ruth), 1964- Springer-Verlag	12 図書 Object-oriented programming in C++ Barkakati, Nabajyoti, 1956- Sams