| Document Type
|
:
|
BL
|
| Record Number
|
:
|
727165
|
| Doc. No
|
:
|
b546897
|
| Main Entry
|
:
|
John V. Guttag; James J. Horning. With S.J. Garland ...
|
| Title & Author
|
:
|
Larch Languages and Tools for Formal Specification\ John V. Guttag; James J. Horning. With S.J. Garland ...
|
| Edition Statement
|
:
|
Softcover reprint of the hardcover 1st ed. 1993
|
| Publication Statement
|
:
|
New York, NY [u.a.] Springer, [2012?]
|
| Series Statement
|
:
|
Texts and Monographs in Computer Science
|
| Page. NO
|
:
|
XIII, 250 S
|
| ISBN
|
:
|
1461276365
|
|
|
:
|
: 9781461276364
|
| 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.
|
| Subject
|
:
|
Algebraische Spezifikation
|
| Subject
|
:
|
LARCH
|
| Subject
|
:
|
Softwareentwicklung
|
| LC Classification
|
:
|
QA76.6J646 2012
|
| Added Entry
|
:
|
James J Horning
|
|
|
:
|
John V Guttag
|