Atjaunināt sīkdatņu piekrišanu

Specification of Software Systems [Hardback]

,
  • Formāts: Hardback, 442 pages, height x width x depth: 178x254x25 mm, weight: 1065 g, 88 black & white illustrations
  • Sērija : Texts in Computer Science
  • Izdošanas datums: 28-Sep-1998
  • Izdevniecība: Springer-Verlag New York Inc.
  • ISBN-10: 0387984305
  • ISBN-13: 9780387984308
Citas grāmatas par šo tēmu:
Specification of Software SystemsPalielināt
  • Formāts: Hardback, 442 pages, height x width x depth: 178x254x25 mm, weight: 1065 g, 88 black & white illustrations
  • Sērija : Texts in Computer Science
  • Izdošanas datums: 28-Sep-1998
  • Izdevniecība: Springer-Verlag New York Inc.
  • ISBN-10: 0387984305
  • ISBN-13: 9780387984308
Citas grāmatas par šo tēmu:
Permanent link: https://www.kriso.lv/db/9780387984308.html
Keywords:
This book provides an introduction to program specification, illustrating the advantages it confers upon the software development process. Covering all three major specification languages (Larch, VDM, and Z), the book discusses specification in general, the abstraction process, the mathematical tools required, and the main formal methods.

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.
Preface v
1 The Role of Specification
1(12)
1.1 Software Complexity
2(3)
1.1.1 Size Complexity
3(1)
1.1.2 Structural Complexity
3(1)
1.1.3 Environmental Complexity
4(1)
1.1.4 Application Domain Complexity
4(1)
1.1.5 Communication Complexity
5(1)
1.2 Software Specification
5(4)
1.2.1 What Is a Specification?
5(3)
1.2.2 How to Control Complexity?
8(1)
1.2.3 A Critique of Natural Language Specification
9(1)
Exercises
9(1)
Bibliographic Notes
10(1)
References
10(3)
2 Specification Activities
13(10)
2.1 Integrating Formal Methods into the Software Life Cycle
14(2)
2.2 Administrative and Technical Roles
16(3)
2.2.1 Specification Roles
17(1)
2.2.2 Design Roles
18(1)
2.2.3 Programming Roles
19(1)
Exercises
19(1)
Bibliographic Notes
20(1)
References
20(3)
3 Specification Qualities
23(8)
3.1 Principles of Software Specifications
23(3)
3.2 Attributes for Specification Languages
26(3)
Exercises
29(1)
Bibliographic Notes
30(1)
References
30(1)
4 Abstraction
31(8)
4.1 What Is Abstraction?
31(1)
4.2 Abstractions in Mathematics
32(1)
4.3 Fundamental Abstractions in Computing
32(3)
4.4 Abstractions for Software Construction
35(2)
Exercises
37(1)
Bibliographic Notes
38(1)
References
38(1)
5 Formal Systems
39(40)
5.1 Peano's Axiomatization of Naturals
40(1)
5.2 Model and Theory
41(2)
5.2.1 Formalization in Engineering
41(1)
5.2.2 Formalization in Science
42(1)
5.2.3 Formalization Process in Software Engineering
42(1)
5.3 Components of a Formal System
43(5)
5.3.1 Syntax
43(1)
5.3.2 Semantics
44(1)
5.3.3 Inference Mechanism
45(3)
5.4 Properties of Formal Systems
48(2)
5.4.1 Consistency
48(1)
5.4.2 Completeness
49(1)
5.4.3 Decidability
49(1)
5.5 Two Formal Notations
50(23)
5.5.1 Extended Syntactic Metalanguage
50(3)
5.5.2 Extended Finite State Machine
53(20)
5.6 Formal Specification Methods--A Classification
73(1)
Exercises
74(2)
Bibliographic Notes
76(1)
References
77(2)
6 Logic
79(58)
6.1 Propositional Logic
79(9)
6.1.1 Syntax and Semantics
80(1)
6.1.2 Proofs
81(7)
6.2 Predicate Logic
88(21)
6.2.1 Syntax and Semantics
88(6)
6.2.2 More on Quantified Expressions
94(3)
6.2.3 Proofs
97(5)
6.2.4 More Specification Examples
102(7)
6.3 Temporal Logic
109(23)
6.3.1 Concurrent and Reactive Systems
110(1)
6.3.2 The Notion of Time
111(1)
6.3.3 The Specification Hierarchy
112(1)
6.3.4 Temporal Logic--Syntax and Semantics
112(5)
6.3.5 Specifications
117(15)
Exercises
132(2)
Bibliographic Notes
134(1)
References
135(2)
7 Set Theory and Relations
137(34)
7.1 Formal Specification Based on Set Theory
137(9)
7.1.1 Set Notation
138(1)
7.1.2 Reasoning with Sets
139(2)
7.1.3 A Specification Example
141(5)
7.2 Formal Specification Based on Relations and Functions
146(13)
7.2.1 Relations and Functions
146(3)
7.2.2 Functions on Relations
149(3)
7.2.3 Reasoning
152(4)
7.2.4 A Specification Example
156(3)
7.3 Formal Specification Based on Sequences
159(8)
7.3.1 Notation
159(1)
7.3.2 Sequence Operators
159(3)
7.3.3 Proofs
162(4)
7.3.4 A Specification Example
166(1)
Exercises
167(2)
Bibliographic Notes
169(1)
References
169(2)
8 Algebraic Specification
171(48)
8.1 Algebra and Specification
171(3)
8.2 Algebras--A Brief Introduction
174(3)
8.2.1 Homomorphisms
175(2)
8.3 Abstract Data Types
177(4)
8.3.1 Presentation
178(2)
8.3.2 Semantics
180(1)
8.4 Properties of Algebraic Specifications
181(7)
8.4.1 Reasoning
181(3)
8.4.2 Extending Many-Sorted Specifications
184(1)
8.4.3 Classification of Operations
184(2)
8.4.4 Adequacy
186(2)
8.5 Structured Specifications
188(4)
8.6 OBJ3--An Algebraic Specification Language
192(9)
8.6.1 Basic Syntax
194(2)
8.6.2 Built-In Sorts and Subsorts
196(5)
8.7 Signature and Equations
201(2)
8.8 Parameterized Programming
203(6)
8.8.1 Theories
203(1)
8.8.2 Views
204(1)
8.8.3 Parameterized Modules
204(1)
8.8.4 Instantiation
205(3)
8.8.5 Module Expression
208(1)
8.9 Case Study--A Multiple Window Environment
209(6)
Exercises
215(1)
Bibliographic Notes
216(1)
References
217(2)
9 Vienna Development Method
219(62)
9.1 Structure of a VDM Specification
219(2)
9.2 Representational Abstraction
221(16)
9.2.1 Identifiers
221(1)
9.2.2 Simple Types
222(1)
9.2.3 Composite Types
223(9)
9.2.4 Patterns, Bindings, and Values
232(2)
9.2.5 State Representation
234(2)
9.2.6 Invariants
236(1)
9.3 Operational Abstraction
237(6)
9.3.1 Let Expression
238(1)
9.3.2 Function Definitions
238(3)
9.3.3 Operation Definitions
241(2)
9.4 Statements
243(3)
9.5 Specification Examples
246(11)
9.6 Case Study--Computer Network
257(8)
9.7 Rigorous Reasoning
265(2)
9.8 Refinement and Proof Obligations
267(7)
9.8.1 Data Refinement
267(2)
9.8.2 Example for Data Refinement
269(2)
9.8.3 Operation Decomposition
271(1)
9.8.4 Example for Operation Decomposition
272(2)
Exercises
274(3)
Bibliographic Notes
277(1)
References
278(3)
10 The Z Notation
281(80)
10.1 A Brief Overview of Z
281(1)
10.2 Representational Abstraction
282(20)
10.2.1 Types
283(2)
10.2.2 Abbreviation
285(1)
10.2.3 Relations and Functions
285(2)
10.2.4 Sequences
287(1)
10.2.5 Bags
287(4)
10.2.6 Free Types
291(1)
10.2.7 Schemas
292(9)
10.2.8 State Representation
301(1)
10.3 Operational Abstraction
302(9)
10.3.1 Operations
303(2)
10.3.2 Schema Decorators and Conventions
305(2)
10.3.3 Sequential Composition
307(2)
10.3.4 Functions
309(2)
10.4 Specification Examples
311(16)
10.5 Proving Properties from Z Specifications
327(8)
10.5.1 Initial State Validation
327(3)
10.5.2 Consistency of Operations
330(5)
10.6 Case Study--An Automated Billing System
335(8)
10.7 Additional Features in Z
343(5)
10.7.1 Precondition Calculation
343(2)
10.7.2 Promotion
345(3)
10.8 Refinement and Proof Obligations
348(8)
10.8.1 Data Refinement
348(5)
10.8.2 Proof Obligations
353(3)
Exercises
356(2)
Bibliographic Notes
358(1)
References
359(2)
11 Larch
361(56)
11.1 The Two Tiers of Larch
362(1)
11.2 LSL--Larch Shared Language
363(14)
11.2.1 Equational Specification
363(4)
11.2.2 More Expressive Specifications and Stronger Theories
367(3)
11.2.3 Composing Traits
370(1)
11.2.4 Renaming
371(1)
11.2.5 Stating Checkable Properties
371(2)
11.2.6 Stating Assumptions
373(2)
11.2.7 Operator Overloading
375(1)
11.2.8 In-line Traits
376(1)
11.3 More LSL Examples
377(13)
11.3.1 File
378(2)
11.3.2 Iterator
380(3)
11.3.3 Date and Zone
383(4)
11.3.4 Time
387(3)
11.4 Larch/C++: A Larch Interface Specification Language for C++
390(10)
11.4.1 Relating Larch/C++ to C++
392(5)
11.4.2 Function Specification
397(2)
11.4.3 Additional Function Specification Features
399(1)
11.5 Proofs in LSL
400(6)
11.5.1 Proof Obligations
400(2)
11.5.2 LP: Larch Proof Assistant
402(4)
11.6 Case Study--Two Examples from Rogue Wave Library
406(7)
11.6.1 RWZone Specification
409(1)
11.6.2 RWFile Specification
409(4)
Exercises
413(2)
Bibliographic Notes
415(1)
References
416(1)
Index 417