Modular Specification and Verification of Object-Oriented Programs

>> Google Books

Modular Specification and Verification of Object-Oriented Programs / Peter Müller

資料種別:: 電子ブック
出版情報:: SpringerLink Books - AutoHoldings
Springer Berlin Heidelberg, 2002
著者名:: Müller, Peter
ISBN:: 9783540431671 [3540431675]
9783540456513 [3540456511]
書誌ID:: OB00499983

子書誌情報

フルテキスト

所蔵情報

書誌詳細

言語:

英語

目次情報:

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 Springer	7 図書 Research directions in object-oriented programming Shriver, Bruce D., 1940-, Wegner, Peter MIT Press
2 図書 Object-oriented programming ([text] ; computer disk) Coad, Peter, Nicola, Jill Prentice-Hall International	8 電子ブック Modular Compiler Verification Müller-Olm, Markus SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg
3 図書 Algebraic specification techniques in object oriented programming environments (: gw ; : us) Breu, R. (Ruth), 1964- Springer-Verlag	9 電子ブック Verification of Object-Oriented Software. The KeY Approach Beckert, Bernhard, Carbonell, Jaime G., H?hnle, Reiner, Schmitt, Peter H., Siekmann, J?rg Springer eBooks Computer Science, Springer Berlin Heidelberg
4 電子ブック Algebraic Specification Techniques in Object Oriented Programming Environments Breu, Ruth SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg	10 電子ブック Verification of Object-Oriented Software. The KeY Approach Beckert, Bernhard, Carbonell, Jaime G., Hähnle, Reiner, Schmitt, Peter H., Siekmann, Jörg SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg
5 電子ブック Aliasing in Object-Oriented Programming. Types, Analysis and Verification Hutchison, David; Kanade, Takeo; Kittler, Josef Springer eBooks Computer Science, Springer Berlin Heidelberg	11 電子ブック Proceedings of the 1986 SIGPLAN workshop on Object-oriented programming Wegner, Peter, Association for Computing Machinery-Digital Library. ACM Digital Library Proceedings, ACM
6 電子ブック Aliasing in Object-Oriented Programming. Types, Analysis and Verification Hutchison, David; Kanade, Takeo; Kittler, Josef, Noble, James, Wrigstad, Tobias SpringerLink Books - AutoHoldings, Springer Berlin Heidelberg	12 図書 Object-oriented behavioral specifications Kilov, Haim, Harvey, William, 1938- Kluwer Academic Publishers