Promotional Information

Springer Book Archives

Table of Contents

1 Specifications in Program Development.- 1.1 Programming with abstractions.- 1.2 Finding abstractions.- 1.3 The many roles of specification.- 1.4 Styles of specification.- 1.5 Formal specifications.- 2 A Little Bit of Logic.- 2.1 Basic logical concepts.- 2.2 Proof and consequences.- 3 An Introduction to Larch.- 3.1 Two-tiered specifications.- 3.2 LSL, the Larch Shared Language.- 3.3 Interface specifications.- 3.4 Relating implementations to specifications.- 3.5 LP, the Larch proof assistant.- 3.6 Lexical and typographic conventions.- 4 LSL: The Larch Shared Language.- 4.1 Equational specifications.- 4.2 Stronger theories.- 4.3 Combining traits.- 4.4 Renaming.- 4.5 Stating intended consequences.- 4.6 Recording assumptions.- 4.7 Built-in operators and overloading.- 4.8 Shorthands.- 4.9 Further examples.- 5 LCL: A Larch Interface Language for C.- 5.1 The relation between LCL and C.- 5.2 Function specifications.- 5.3 A guided tour through an LCL specification.- 6 LM3: A Larch Interface Language for Modula-3.- 6.1 The relation between LM3 and Modula-3.- 6.2 The LM3 semantic model.- 6.3 A guided tour through an LM3 specification.- 7 Using LP to Debug LSL Specifications.- 7.1 Semantic checks in LSL.- 7.2 Proof obligations for LSL specifications.- 7.3 Translating LSL traits into LP.- 7.4 Proof mechanisms in LP.- 7.5 Checking theory containment.- 7.6 Checking consistency.- 7.7 Extended example.- 7.8 Perspective.- 8 Conclusion.- A An LSL Handbook.- A.1 Introduction.- A.2 Foundations.- A.3 Integers.- A.4 Enumerations.- A.5 Containers.- A.6 Branching structures.- A.7 Maps.- A.8 Relations.- A.9 Graph theory.- A.10 Properties of single operators.- A.11 Properties of relational operators.- A.12 Orderings.- A.13 Lattice theory.- A.14 Group theory.- A.15 Number theory.- A.16 Floating point arithmetic.- B Implementations of Example LCL Interfaces.- C Lexical Forms and Initialization Files.- D Further Information and Tools.- E Classified Bibliography.- References.