We will be undergoing system maintenance on May 16th, 2024 from 2 am through 6 am central time. The system will be unavailable during that time. Please plan accordingly.
Software Abstractions, Revised Edition
Logic, Language, and Analysis
by Jackson
ISBN: 9780262300254 | Copyright 2011
Instructor Requests
In Software Abstractions Daniel Jackson introduces an approach to software design that draws on traditional formal methods but exploits automated tools to find flaws as early as possible. This approach—which Jackson calls “lightweight formal methods” or “agile modeling”—takes from formal specification the idea of a precise and expressive notation based on a tiny core of simple and robust concepts but replaces conventional analysis based on theorem proving with a fully automated analysis that gives designers immediate feedback. Jackson has developed Alloy, a language that captures the essence of software abstractions simply and succinctly, using a minimal toolkit of mathematical notions. This revised edition updates the text, examples, and appendixes to be fully compatible with Alloy 4.
| Expand/Collapse All | |
|---|---|
| Contents (pg. vii) | |
| Preface (pg. xi) | |
| Acknowledgments (pg. xv) | |
| Acknowledgments (revised edition) (pg. xvii) | |
| Chapter 1: Introduction (pg. 1) | |
| Chapter 2: A Whirlwind Tour (pg. 5) | |
| 2.1 Statics: Exploring States (pg. 6) | |
| 2.2 Dynamics: Adding Operations (pg. 9) | |
| 2.3 Classification Hierarchy (pg. 17) | |
| 2.4 Execution Traces (pg. 22) | |
| 2.5 Summary (pg. 28) | |
| Chapter 3: Logic (pg. 33) | |
| 3.1 Three Logics in One (pg. 33) | |
| 3.2 Atoms and Relations (pg. 35) | |
| 3.3 Snapshots (pg. 48) | |
| 3.4 Operators (pg. 50) | |
| 3.5 Constraints (pg. 68) | |
| 3.6 Declarations and Multiplicity Constraints (pg. 75) | |
| 3.7 Cardinality and Integers (pg. 80) | |
| Chapter 4: Language (pg. 85) | |
| 4.1 An Example: Self-Grandpas (pg. 85) | |
| 4.2 Signatures and Fields (pg. 93) | |
| 4.3 Model Diagrams (pg. 103) | |
| 4.4 Types and Type Checking (pg. 109) | |
| 4.5 Facts, Predicates, Functions, and Assertions (pg. 119) | |
| 4.6 Commands and Scope (pg. 130) | |
| 4.7 Modules and Polymorphism (pg. 133) | |
| Chapter 5: Analysis (pg. 141) | |
| 5.1 Scope-Complete Analysis (pg. 141) | |
| 5.2 Instances, Examples, and Counterexamples (pg. 146) | |
| 5.3 Unbounded Universal Quantifiers (pg. 157) | |
| 5.4 Scope Selection and Monotonicity (pg. 165) | |
| Chapter 6: Examples (pg. 171) | |
| 6.1 Leader Election in a Ring (pg. 171) | |
| 6.2 Hotel Room Locking (pg. 187) | |
| 6.3 Media Asset Management (pg. 205) | |
| 6.4 Memory Abstractions (pg. 219) | |
| Appendix A: Exercises (pg. 233) | |
| A.1 Logic Exercises (pg. 234) | |
| A.2 Extending Simple Models (pg. 244) | |
| A.3 Classic Puzzles (pg. 247) | |
| A.4 Metamodels (pg. 250) | |
| A.5 Small Case Studies (pg. 251) | |
| A.6 Open-Ended Case Studies (pg. 256) | |
| Appendix B: Alloy Language Reference (pg. 259) | |
| B.1 Lexical Issues (pg. 259) | |
| B.2 Namespaces (pg. 260) | |
| B.3 Grammar (pg. 261) | |
| B.4 Precedence and Associativity (pg. 263) | |
| B.5 Semantic Basis (pg. 264) | |
| B.6 Types and Overloading (pg. 266) | |
| B.7 Language Features (pg. 270) | |
| B.8 Relational Expressions (pg. 285) | |
| B.9 Integer Expressions (pg. 288) | |
| Appendix C: Kernel Semantics (pg. 295) | |
| C.1 Semantics of the Alloy Kernel (pg. 295) | |
| Appendix D: Diagrammatic Notation (pg. 299) | |
| Appendix E: Alternative Approaches (pg. 301) | |
| E.1 An Example (pg. 303) | |
| E.2 B (pg. 310) | |
| E.3 OCL (pg. 316) | |
| E.4 VDM (pg. 322) | |
| E.5 Z (pg. 328) | |
| References (pg. 337) | |
| Index (pg. 345) | |
| Symbols (pg. 345) | |
| A (pg. 345) | |
| B (pg. 346) | |
| C (pg. 346) | |
| D (pg. 346) | |
| E (pg. 347) | |
| F (pg. 347) | |
| G (pg. 348) | |
| H (pg. 348) | |
| I (pg. 348) | |
| J (pg. 349) | |
| K (pg. 349) | |
| L (pg. 349) | |
| M (pg. 350) | |
| N (pg. 350) | |
| O (pg. 350) | |
| P (pg. 351) | |
| Q (pg. 351) | |
| R (pg. 352) | |
| S (pg. 352) | |
| T (pg. 353) | |
| U (pg. 354) | |
| V (pg. 354) | |
| W (pg. 354) | |
| Z (pg. 354) | |
Daniel Jackson
Daniel Jackson is Professor in the Department of Electrical Engineering and Computer Science and leads the Software Design Group at the Computer Science and Artificial Intelligence Lab at MIT.
|
eTextbook
Go paperless today! Available online anytime, nothing to download or install.
|
