1 Introduction. - 1. 1 The Problems and the Approach. - 1. 2 Larch/C Interface Language. - 1. 3 Related Work. - 1. 4 Key Lessons Learned. - 1. 5 Research Contributions. - 2 Overview of LCL. - 2. 1 Larch. - 2. 2 LCL Basics. - 2. 3 LCL Function Specification. - 2. 4 LCL Abstract Type Specification. - 2. 5 Historical Note. - 3 Supporting Programming Styles. - 3. 1 Specified Interfaces and Data Abstraction. - 3. 2 Specified Interfaces in C. - 3. 3 Abstract Types in C. - 3. 4 Tool Support: LCLint. - 3. 5 Summary. - 4 Specification Techniques. - 4. 1 Requirements of the Program. - 4. 2 The Design of the PM Program. - 4. 3 Overview of Specification Techniques. - 4. 4 The date Interface. - 4. 5 The trans Traits. - 4. 6 The trans Interface. - 4. 7 The trans-set Interface and Trait. - 4. 8 The position Traits. - 4. 9 The position Interface. - 4. 10 Summary. - 5 Redundancy in Specifications. - 5. 1 Testing Specifications. - 5. 2 Semantics of Claims. - 5. 3 Claims Help Test Specifications. - 5. 4 Claims Help Specification Regression Testing. - 5. 5 Claims Highlight Specification Properties. - 5. 6 Claims Promote Module Coherence. - 5. 7 Claims Support Program Reasoning. - 5. 8 Claims Support Test Case Generation. - 5. 9 Experiences in Checking LCL Claims. - 5. 10 Claims or Axioms?. - 5. 11 Summary. - 6 Reengineering Using LCL. - 6. 1 Software Reengineering Process Model. - 6. 2 A Reengineering Exercise. - 6. 3 Effects of Reengineering. - 6. 4 Specification Tool Support. - 6. 5 Summary. - 7 The Semantics of LCL. - 7. 1 Basic LCL Concepts. - 7. 2 LCL Storage Model. - 7. 3 LCL Type System. - 7. 4 LCL Function Specification. - 7. 5 LCL Module. - 7. 6 Type Safety of Abstract Types. - 7. 7 Summary. - 8 Further Work and Summary. - 8. 1 Further Work. - 8. 2 Summary. - A LCL Reference Grammar. - B Relating LCL Types and LSL Sorts. - B. 1 Modeling LCL Exposed Types with LSL Sorts. - B. 2 Assigning LSLSorts to LCL Variables. - B. 3 Assigning LSL Sorts to C Literals. - C LCL Built-In Operators. - D Specification Case Study. - D. 1 The char Trait. - D. 2 The cstring Trait. - D. 3 The string Trait. - D. 4 The mystdio Trait. - D. 5 The genlib Trait. - D. 6 The dateBasics Trait. - D. 7 The dateFormat Trait. - D. 8 The date Trait. - D. 9 The security Trait. - D. 10 The lot Trait. - D. 11 The list Trait. - D. 12 The lot list Trait. - D. 13 The kind Trait. - D. 14 The transBasics Trait. - D. 15 The transFormat Trait. - D. 16 The transParse Trait. - D. 17 The trans Trait. - D. 18 The trans-set Trait. - D. 19 The income Trait. - D. 20 The positionBasics Trait. - D. 21 The positionMatches Trait. - D. 22 The positionExchange Trait. - D. 23 The positionReduce Trait. - D. 24 The positionSell Trait. - D. 25 The positionTbill Trait. - D. 26 The position Trait. - D. 27 The genlib Interface. - D. 28 The date Interface. - D. 29 The security Interface. - D. 30 The lot-list Interface. - D. 31 The trans Interface. - D. 32 The trans_set Interface. - D. 33 The position Interface. - E Getting Larch Tools and Information. - References. Language: English