Specification of Software Systems

Front Cover
Springer Science & Business Media, 1998 - Computers - 422 pages
This graduate-level text provides a one semester introduction to program specification. Readers are assumed to have a working knowledge of software engineering and basic discrete mathematics, but otherwise this may be their first encounter with formal specification. It is based on graduate courses and courses offered to professionals working in the software industry. The authors emphasize the need for formal abstraction in specification and the advantages it confers upon the software process. In addition, the book covers all three major specification languages: Larch, VDM, and Z. Consequently, readers will be able to select a formal method that best suits their needs and application. The first part of the book discusses specification in general and the abstraction process. Next come chapters on the mathematical tools required. Thirdly, the authors devote a chapter each to the main formal methods with a significant example of the use of each discussed.
 

What people are saying - Write a review

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

Contents

The Role of Specification
1
11 Software Complexity
2
111 Size Complexity
3
113 Environmental Complexity
4
115 Communication Complexity
5
122 How to Control Complexity?
8
123 A Critique of Natural Language Specification
9
Bibliographic Notes
10
88 Parameterized Programming
203
882 Views
204
884 Instantiation
205
885 Module Expression
208
89 Case StudyA Multiple Window Environment
209
Exercises
215
Bibliographic Notes
216
References
217

Specification Activities
13
21 Integrating Formal Methods into the Software Life Cycle
14
22 Administrative and Technical Roles
16
221 Specification Roles
17
222 Design Roles
18
223 Programming Roles
19
Bibliographic Notes
20
Specification Qualities
23
32 Attributes for Specification Languages
26
Exercises
29
Bibliographic Notes
30
Abstraction
31
42 Abstractions in Mathematics
32
44 Abstractions for Software Construction
35
Exercises
37
Bibliographic Notes
38
Formal Systems
39
51 Peanos Axiomatization of Naturals
40
52 Model and Theory
41
522 Formalization in Science
42
53 Components of a Formal System
43
532 Semantics
44
533 lnference Mechanism
45
54 Properties of Formal Systems
48
542 Completeness
49
55 Two Formal Notations
50
552 Extended Finite State Machine
53
56 Formal Specification MethodsA Classification
73
Exercises
74
Bibliographic Notes
76
References
77
Logic
79
611 Syntax and Semantics
80
612 Proofs
81
62 Predicate Logic
88
622 More on Quantified Expressions
94
623 Proofs
97
624 More Specification Examples
102
63 Temporal Logic
109
631 Concurrent and Reactive Systems
110
632 The Notion of Time
111
633 The Specification Hierarchy
112
635 Specifications
117
Exercises
132
Bibliographic Notes
134
References
135
Set Theory and Relations
137
711 Set Notation
138
712 Reasoning with Sets
139
713 A Specification Example
141
72 Formal Specification Based on Relations and Functions
146
722 Functions on Relations
149
723 Reasoning
152
724 A Specification Example
156
73 Formal Specification Based on Sequences
159
733 Proofs
162
734 A Specification Example
166
Exercises
167
Bibliographic Notes
169
Algebraic Specification
171
82 AlgebrasA Brief Introduction
174
821 Homomorphisms
175
83 Abstract Data Types
177
831 Presentation
178
832 Semantics
180
84 Properties of Algebraic Specifications
181
842 Extending ManySorted Specifications
184
844 Adequacy
186
85 Structured Specifications
188
86 OBJ3An Algebraic Specification Language
192
861 Basic Syntax
194
862 Builtin Sorts and Subsorts
196
87 Signature and Equations
201
Vienna Development Method
219
92 Representational Abstraction
221
922 Simple Types
222
923 Composite Types
223
924 Patterns Bindings and Values
232
925 State Representation
234
926 Invariants
236
93 Operational Abstraction
237
931 Let Expression
238
933 Operation Definitions
241
94 Statements
243
95 Specification Examples
246
96 Case StudyComputer Network
257
97 Rigorous Reasoning
265
98 Refinement and Proof Obligations
267
982 Example for Data Refinement
269
983 Operation Decomposition
271
984 Example for Operation Decomposition
272
Exercises
274
Bibliographic Notes
277
References
278
The Z Notation
281
102 Representational Abstraction
282
1021 Types
283
1022 Abbreviation
285
1024 Sequences
287
1026 Free Types
291
1027 Schemas
292
1028 State Representation
301
103 Operational Abstraction
302
1031 Operations
303
1032 Schema Decorators and Conventions
305
1033 Sequential Composition
307
1034 Functions
309
104 Specification Examples
311
105 Proving Properties from Z Specifications
327
1052 Consistency of Operations
330
106 Case StudyAn Automated Billing System
335
107 Additional Features in Z
343
1072 Promotion
345
108 Refinement and Proof Obligations
348
1082 Proof Obligations
353
Exercises
356
Bibliographic Notes
358
References
359
Larch
361
111 The Two Tiers of Larch
362
112 LSLLarch Shared Language
363
1122 More Expressive Specifications and Stronger Theories
367
1123 Composing Traits
370
1124 Renaming
371
1126 Stating Assumptions
373
1127 Operator Overloading
375
1128 Inline Traits
376
113 More LSL Examples
377
1131 File
378
1132 Iterator
380
1133 Date and Zone
383
1134 Time
387
A Larch Interface Specification Language for C++
390
1141 Relating LarchC++ to C++
392
1142 Function Specification
397
1143 Additional Function Specification Features
399
115 Proofs in LSL
400
Larch Proof Assistant
402
116 Case StudyTwo Examples from Rogue Wave Library
406
1161 RWZone Specification
409
Exercises
413
Bibliographic Notes
415
References
416
Index
417
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information