Modular Specification and Verification of Object-Oriented Programs (Google eBook)

Front Cover
Peter Müller
Springer Science & Business Media, Jan 23, 2002 - Computers - 292 pages
0 Reviews
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.
  

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

1 Introduction
1
11 Motivation
2
12 Specification and Verification Technique
4
13 The Problem
5
131 Modular Correctness
7
132 The Frame Problem
8
133 Modular Verification of Type Invariants
10
134 The Extended State Problem
11
51 Approach
144
511 Meaning of ModifiesClauses
145
512 Explicit Dependencies
147
513 Modularity Rules
148
52 Formalization of Explicit Dependencies
155
521 Declaration of Dependencies
156
523 Consistency with Representation
157
524 Formalization of the Modularity Rules
159

135 Alias Control
13
14 Modularity Aspects of Programs Specifications and Proofs
16
141 Modularity of Programs
17
142 Modularity of Universal Specifications
21
143 Modularity of Interface Specifications
22
144 Modularity of Correctness Proofs
26
15 Approach Outline and Contributions
28
152 Outline
31
153 Contributions
32
16 Related Work
33
162 Verification and Analysis Techniques
36
2 Mojave and the Universe Type System
39
212 Modularity
45
A Type System for Flexible Alias Control
51
221 The Ownership Model
52
222 The Universe Programming Model
54
223 Programming with Universes
58
224 Examples
60
225 Formalization of the Universe Type System
66
226 Discussion
70
23 Related Work
74
3 The Semantics of Mojave
77
312 Axiomatic Semantics
92
313 Programming Logic
97
321 Type Safety
99
322 Liveness Properties
108
323 Properties of Readonly Methods
109
33 Correctness
110
333 Modular Soundness
112
34 Related Work
120
4 Modular Specification and Verification of Functional Behavior
123
42 Specification of Functional Behavior
125
422 Prepostspecifications
131
43 Verification of Functional Behavior
135
432 Proofs for Virtual Methods
136
433 Example
137
44 Related Work
139
442 Verification of Functional Behavior
141
5 Modular Specification and Verification of Frame Properties
143
525 Axiomatization of the NotdependsRelation
160
526 Example
167
527 Discussion
169
53 Formalization of ModifiesClauses
176
54 Verification of Frame Properties
178
542 Local Update Property
180
543 Accessibility Properties
181
544 Modularity Theorem for Frame Properties
183
545 Example
184
55 Related Work
188
552 Other Work on the Frame Problem
193
6 Modular Specification and Verification of Type Invariants
195
612 Problems for Modular Verification of Invariants
197
613 Approach
198
62 Specification of Type Invariants
201
622 Example
203
623 Formal Meaning of Invariants
204
631 Verification Methodology
205
632 Example
206
64 Discussion
207
642 History Constraints
208
65 Related Work
209
7 Conclusion
213
72 The Lopex Project
217
74 Directions for Future Work
219
A Formal Background and Notations
223
A2 Notations
225
B Predefined Type Declarations
227
C Examples
229
C2 Property Editor
235
D Auxiliary Lemmas Proofs and Models
237
D2 Auxiliary Lemmas and Proofs from Chapter 5
243
D3 Auxiliary Lemmas and Proofs from Chapter 6
261
D4 A Model for the Axiomatization of the DependsRelation
266
Bibliography
271
List of Figures
285
Index
287
Copyright

Common terms and phrases

Popular passages

Page 1 - Life is like a box of chocolates... You never know what you're gonna get.
Page 277 - [LW90] GT Leavens and WE Weihl. Reasoning about object-oriented programs that use subtypes (extended abstract). In N. Meyrowitz, editor, OOPSLA ECOOP '90 Proceedings, volume 25(10) of

Bibliographic information