Software Abstractions: Logic, Language, and Analysis
- 2025-04-26 (modified: 2025-07-13)
- 저자: Daniel Jackson
Preface
The experience of exploring a software model with an automatic analyzer is at once thrilling and humiliating. Most modelers have had the benefit of review by colleagues; it’s a sure way to find flaws and catch omissions. Few modelers, however, have had the experience of subjecting their modes to continual, automatic review. … The first reaction tends to be amazement: modeling is much more fun when you get instant, visual feedback. … Then the sense of humiliation sets in, as you discover that there’s almost nothing you can do right. What you write down doesn’t mean exactly what you think it means. And when it does, it doesn’t have the consequences you expected. … Slowly but surely the tool teaches you to make fewer and fewer errors. Your sense of confidence in your modeling ability (and in your models!) grows.
소프트웨어의 기저에 놓인 “개념(concepts)“의 중요성. The Essence of Software로 이어지는 내용:
The Alloy language and its analysis are a Trojan horse: an attempt to capture the attention of software developers, who are mired in the tar pit of implementation technologies, and to bring them back to thinking deeply about underlying concepts.
1. Introduction
Extreme programming의 장점과 한계:
Recognizing the advantage of early application of tools, and the risk of wishful thinking, the approach known as “Extreme programming” eliminates design as a separate phase altogether. The design of the software eolves with the code, kept in check by the rigors of type checking and unit tests. But code is a poor medium for exploring abstractions.
2. A Whirlwind Tour
Most flaws in models can be illustrated by small instances, since they arise from some shape being handled incorrectly, and whether the shape belongs to a large or small instances, most flaws will be revealed. This observation, which I call the small scope hypothesis, is the fundamental premise that underlies Alloy’s analysis.
3. Logic
Three logics in one
In the predicate calculus style, there are only two kinds of expression: relation names, which are used as predicates, and tuples formed from quantified variables. …
In the navigation expression style, expressions denote sets, which are formed by “navigating” from quantified variables along relations. …
In the relational calculus style, expressions denote relations, and there are no quantifiers at all.
Comparison
Predicate calculus style:
all n: Name, d, d': Address |
n->d in address and n->d' in address implies d=d'
Navigation expression style:
all n: Name | lone n.address
Relational calculus style:
no ~address.address - iden
Does the styles have equivalent expressive power?
No. The navigational style is the most expressive. Predicate calculus lacks transitive closure, so reachability properties can’t be expressed. The relational calculus has no quantifiers, and not all occurrences of the quantifiers of predicate calculus can be expressed purely relationally.
Is the idea of treating scalars and sets as relations new?
No. It goes back to Tarski’s foundational work on the relational calculus. All of Tarski’s relations were binary, however, so his encoding was a lit less natural: a set was a relation that mapped each atom in the set to every possible atom.
Functional and injective relations
Example:
// functional but not injective
addr1 = {(N0, D0), {N1, D1}, {N2, D1}}
// injective but not functional
addr2 = {(N0, D0), (N1, D1), (N1, D2)}
// functional and injective
addr = {(N0, D0), (N1, D1), (N2, D2)}
// neither
addr = {(N0, D1), (N1, D1), (N1, D2)}
Is an injective relation an injection?
The term “injection” is traditionally applied only to a relation that is both functional and injective, so I try to avoid using it. Unformunately, there isn’t a common name for an injective relation.