Software Abstractions: Logic, Language, and Analysis

✍ Scribed by Daniel Jackson

• Publisher: The MIT Press
• Year: 2006
• Tongue: English
• Leaves: 369
• Category: Library

✦ Synopsis

In Software Abstractions Daniel Jackson introduces a new 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. The designer can use automated analysis not only to correct errors but also to make models that are more precise and elegant. This approach, Jackson says, can rescue designers from "the tarpit of implementation technologies" and return them to thinking deeply about underlying concepts. Software Abstractions introduces the key elements of the approach: a logic, which provides the building blocks of the language; a language, which adds a small amount of syntax to the logic for structuring descriptions; and an analysis, a form of constraint solving that offers both simulation (generating sample states and executions) and checking (finding counterexamples to claimed properties). The book uses Alloy as a vehicle because of its simplicity and tool support, but the book's lessons are mostly language-independent, and could also be applied in the context of other modeling languages.

✦ Table of Contents

Cover......Page 1
Contents......Page 8
Preface......Page 12
Acknowledgments......Page 16
1: Introduction......Page 18
2: A Whirlwind Tour......Page 22
2.1 Statics: Exploring States......Page 23
2.2 Dynamics: Adding Operations......Page 26
2.3 Classification Hierarchy......Page 34
2.4 Execution Traces......Page 39
2.5 Summary......Page 45
3.1 Three Logics in One......Page 50
3.2 Atoms and Relations......Page 52
3.3 Snapshots......Page 65
3.4 Operators......Page 67
3.5 Constraints......Page 86
3.6 Declarations and Multiplicity Constraints......Page 91
3.7 Cardinality Constraints......Page 97
4.1 An Example: Self-Grandpas......Page 100
4.2 Signatures and Fields......Page 108
4.3 Model Diagrams......Page 118
4.4 Types and Type Checking......Page 124
4.5 Facts, Predicates, Functions, and Assertions......Page 134
4.6 Commands and Scope......Page 144
4.7 Modules and Polymorphism......Page 147
4.8 Integers and Arithmetic......Page 151
5.1 Scope-Complete Analysis......Page 156
5.2 Instances, Examples, and Counterexamples......Page 161
5.3 Unbounded Universal Quantifiers......Page 172
5.4 Scope Selection and Monotonicity......Page 180
6.1 Leader Election in a Ring......Page 186
6.2 Hotel Room Locking......Page 202
6.3 Media Asset Management......Page 220
6.4 Memory Abstractions......Page 233
Appendix A: Exercises......Page 246
A.1 Logic Exercises......Page 247
A.2 Extending Simple Models......Page 256
A.3 Classic Puzzles......Page 259
A.4 Metamodels......Page 262
A.5 Small Case Studies......Page 264
A.6 Open-Ended Case Studies......Page 268
B.1 Lexical Issues......Page 270
B.2 Namespaces......Page 271
B.3 Grammar......Page 272
B.4 Precedence and Associativity......Page 274
B.5 Semantic Basis......Page 275
B.6 Types and Overloading......Page 277
B.7 Language Features......Page 282
C.1 Semantics of the Alloy Kernel......Page 308
C.2 Semantics of Integer Expressions and Formulas......Page 310
Appendix D: Diagrammatic Notation......Page 312
Appendix E: Alternative Approaches......Page 314
E.1 An Example......Page 316
E.2 B......Page 323
E.3 OCL......Page 329
E.4 VDM......Page 335
E.5 Z......Page 341
References......Page 350
A......Page 358
C......Page 359
F......Page 360
I......Page 361
L......Page 362
O......Page 363
R......Page 364
S......Page 365
T......Page 366
Z......Page 367