| The Science of Software Development | p. 7 |
| Software Engineering as Theory Construction | p. 7 |
| Software Engineering Paradigms | p. 9 |
| The Path from Problem to Program | p. 15 |
| Knowledge-Based Software Development | p. 19 |
| Knowledge Representation as a Basis of Specifying Requirements | p. 28 |
| Demands on a Requirements Specification Language | p. 28 |
| Languages to Formulate Requirements Specifications | p. 32 |
| The FRORL Requirements Specification Language | p. 35 |
| LSSGR Protocol Example | p. 41 |
| Developing Requirements Specifications using FRORL | p. 45 |
| Nonmonotonic Logic Foundation of the Requirements Specification Language | p. 50 |
| The Formal Foundation of FRORL | p. 50 |
| Soundness and Completeness of FRORL | p. 58 |
| Representing FRORL Constructs | p. 65 |
| A Requirements Specification Language for Real-Time Distributed Software Systems | p. 70 |
| Characteristics of Real-Time Distributed Software Systems | p. 70 |
| Demands on Requirements Specification Languages for Real-Time Distributed Systems | p. 71 |
| Languages to Formulate Real-Time Requirements Specifications | p. 73 |
| Modeling Mechanisms for Concurrent Distributed Systems | p. 78 |
| Modeling Constructs for Real-Time Processes, Timing Constraints, and Temporal Properties | p. 81 |
| Temporal Logic Foundation of the Real-Time Distributed Requirements Specification Language | p. 84 |
| The Temporal Fix-Point Calculus | p. 84 |
| Model Checking | p. 89 |
| Expressing the Temporal Aspects of a FRORL Specification | p. 91 |
| Verification of Requirements Specifications | p. 95 |
| Analysis through Resolution Refutation | p. 95 |
| Model Checking | p. 98 |
| Timing Constraints Consistency Analysis | p. 109 |
| Development, Specification, and Verification of Knowledge-Based Systems | p. 117 |
| Difficulties in Verifying Knowledge-Based Systems | p. 117 |
| Correctness Problems in Knowledge Bases | p. 119 |
| Approaches to the Verification of Knowledge-Based Systems | p. 121 |
| Dynamic Verification | p. 126 |
| Knowledge-Based Implementation | p. 136 |
| Automated Program Construction | p. 136 |
| Canonicalization | p. 140 |
| Data Dependency and Control Flow Analysis | p. 154 |
| Determination of Execution Sequence | p. 163 |
| Removal of Unnecessary Nondeterminacy | p. 167 |
| Specification Debugging | p. 174 |
| Knowledge-Based Debugging | p. 174 |
| Debugging of FRORL Specifications | p. 177 |
| A Example Specifications | p. 186 |
| B Formal Grammar of FRORL | p. 197 |
| C Some Results about Fix-Points | p. 200 |
| D References | p. 203 |
| E Index | p. 231 |
| Table of Contents provided by Blackwell. All Rights Reserved. |