Software Blueprints: Lightweight Uses of Logic in Conceptual Modelling
David J. Robertson, Jaumi Agustí · Medical Entomology and Zoology · 1999
Foreword Preface How to read this book Acknowledgements Chapter 1 Introduction 1.1 A dream 1.2 Reality 1.3 Our corner of the problem 1.4 What you can learn from this book 1.5 The way we view conceptual modelling 1.5.1 Models of problems are not specifications of solutions 1.5.2 What we require of conceptual models 1.5.3 Lightweight use of formality 1.5.4 Our use of logic 1.5.5 The need for eclecticism Chapter 2 Models in a design lifecycle 2.1 Requirements analysis 2.2 Choice of representational paradigms 2.2.1 Communication between divisions 2.2.2 Decision procedures within divisions 2.3 Model construction 2.3.1 Communication between divisions 2.3.2 Decision procedures within divisions 2.4 Validation and verification 2.4.1 Validation by analysing potential behaviours 2.4.2 Using our requirements to justify design decisions 2.5 Issues raised by our example 2.5.1 Argumentation networks 2.5.2 More extensive examples using operator models 2.5.3 Conceptual models in knowledge engineering 2.5.4 Model checking Exercises Chapter 3 Logic as a modelling language 3.1 Logics as frameworks for argument 3.2 The boundary problem 3.3 The search problem 3.4 Proof strategies 3.5 Describing proof strategies formally 3.6 Distinguishing proof rules from selection strategies 3.7 Knowing when two terms unify 3.8 The closed world assumption 3.9 Non-deductive patterns of inference 3.9.1 Abduction 3.9.2 Induction 3.10 Ontologies 3.11 Some properties of logical languages 3.11.1 Logical consequence 3.11.2 Correctness and completeness 3.11.3 Decidability 3.11.4 Correctness and completeness of arguments 3.12 Further reading Exercises Chapter 4 Communication 4.1 From domains to formal languages 4.1.1 An entity relationship diagram 4.1.2 A BSDM entity diagram 4.1.3 Lessons from the comparative analysis 4.1.4 Building an early model 4.1.5 Checking the consistency of the model 4.1.6 Lessons learned from more detailed modelling 4.2 From formal languages to domains 4.2.1 Visual formal expressions 4.2.2 Formal problem description by means of diagrams 4.3 The correspondence between logic and diagrams Exercises Chapter 5 Re-use of paradigms: parameterisable components 5.1 Worldwide web site generation 5.1.1 Problem description language (research group) 5.1.2 Parameterisable components (site pages) 5.1.3 Parameterisation system (simple instantiation) 5.1.4 Design generated (web site) 5.2 Rapid domain-specific model generation 5.2.1 Design generated (animal population model) 5.2.2 Parameterisable components (model fragments) 5.2.3 Problem description language (ecological conditions) 5.2.4 Parameterisation system (constrained generation) 5.3 Design endorsements 5.3.1 Problem description language (domain notations) 5.3.2 Design generated (shutdown specification) 5.3.3 Parameterisable components (shutdown segments) 5.3.4 Parameterisation system (design endorsement) 5.4 Costs and benefits 5.5 Further reading Exercises Chapter 6 Design processes inspired by formal methods 6.1 Constructing definitions by slices 6.1.1 Skeletons and additions 6.1.2 A techniques editor at work 6.2 Re-using part of an earlier definition 6.3 Using design histories when combining definitions 6.4 Issues raised by our example 6.4.1 Structured formal definition and transformation 6.4.2 Stripping structure from predicates 6.4.3 Case-based reasoning Exercises Chapter 7 Argumentation 7.1 Reasoning about sources of uncertainty 7.1.1 Reconstructing the model in logic 7.1.2 Reasoning about uncertainty in the model 7.2 Justifying design decisions 7.2.1 Data describing reserve sites 7.2.2 Formal requirements guidelines 7.2.3 Interactively constructing justifications 7.3 Accommodating the dynamics of argument in logic 7.3.1 An example of defeasible argumentation 7.3.2 An abstract argumentation framework 7.4 Further reading Exercises Chapter 8 Temporal reasoning 8.1 Reasoning with temporal intervals 8.2 Modal temporal logic 8.2.1 An example using a 'ticking clock' time sequence 8.2.2 A modal temporal logic for our example 8.2.3 Proofs in modal temporal logic 8.2.4 Other kinds of modal operators 8.3 Reasoning with temporal constraints 8.3.1 Determining when properties hold 8.3.2 Temporal constraint networks 8.4 Further reading Exercises Chapter 9 Syntax, semantics and pragmatics 9.1 Syntax 9.2 Semantics 9.2.1 Linguistic interpretation 9.2.2 A formal semantics for each modelling language 9.2.3 A formal semantics for all modelling languages 9.2.4 Semantics of a family of models within a lifecycle 9.3 Pragmatics Chapter 10 Conclusion 10.1 A summary of our main arguments 10.2 Lightweight tools 10.3 Closing remarks Appendix A Glossary Appendix B Syntax of expressions Appendix C Answers to exercises References