|
Hi Folks, So, you’re creating a data specification. You specify lots of rules and definitions. How will you check to see that they have the desired consequences? You are embarking on a new software project. You desire a development approach that combines the incrementality and immediacy of extreme programming with the depth and clarity of formal specification. Did you know that in recent years there have been tremendous advances in constraint-solving technology (satisfiability, SAT)? The space of cases examined using a SAT tool is usually huge—billions
of cases or more—and SAT therefore offers a degree of coverage unattainable in testing.
Be sure to check your understanding of an application domain before designing an XML representation for objects in that domain. ……………. This article outlines how to express data/software specifications and models succinctly and precisely, in a way that can be automatically analyzed using SAT tools.
Sound interesting? Then check out the example below.
A key to better models, better data specifications, and better software specifications: MIT’s Alloy.
Table of Contents 1. Sample Problem: Design an Email Address Book 2. Address Book, Example #1 3. Address Book, Example #2 4. Only One Place to Change when an Address Changes 5. Sets and Set Relations 6. Instance, State, State Space 7. Address Book Constraints 8. An Alias may be the Target of another Alias 9. Generalize the Concepts 10. Classification Hierarchy 11. (More) Address Book Constraints 12. Model of an Address Book 13. Address Book is a Satisfiability Problem 14. Alloy 15. Alloy Representation of the Address Book Problem 16. Relationship between Alloy and UML 17. Tutorial on Alloy
Sample Problem: Design an Email Address Book An email client’s address book is a little database that associates email addresses with shorter names that are more convenient to use. The user can create an
alias for a correspondent—a nickname that can be used in place of that person’s address, and which need not change when the address itself changes. A
group is like an alias but is associated with an entire set of correspondents—the members of a family, for instance. When defining a group, a user will often insert aliases rather than actual email addresses, so that a change in a person’s email address
can be corrected in just one place, even if it appears implicitly in many groups. [1]
Only One Place to Change when an Address Changes
The set of addresses: The set of aliases: The set of groups: addr is a relation (mapping) between aliases and addresses.
addr(Tom) = tom@foo.com addr(Sara) = sara@foo.com addr(Bill) = bill@foo.com addr(Lynn) = lynn@foo.com Earlier we saw this
instance:
That is one possible
state of an address book. The set of all possible states is the state space.
-
An alias is associated to at most one address. (Can’t associate an alias to multiple addresses)
-
Multiple different aliases may be associated to the same address.
-
Adding to an address book (b) an alias (n) with address (a) results in a new address book (b’) that is the same as the old address book, plus the
n->a mapping.
-
Deleting an alias (n) from an address book (b) results in a new address book (b’) that is the same as the old address book, with all links from the name (n) to any address removed.
An Alias may be the Target of another Alias In a realistic address book application, you can create an alias for an address, and then use that alias as the target for another alias. Example: Eldest is an alias whose target is Tom. Tom is an alias whose target is the address tom@foo.com
Eldest->Tom->tom@foo.com Naming chains of any length are allowed.
Example: Chief->Eldest->Tom->tom@foo.com An Alias is a Name. A Group is a Name. An Address is a Target. Example: in the relation Tom -> tom@foo.com, the address tom@foo.com is the target of the alias Tom.
A Name is a Target. Example: in the relation Eldest -> Tom the name Tom is the target of the name Eldest. Group and Alias is a Name. A Target can be either a Name or an Address.
The addr function maps a Name to a Target.
Target and Name are abstract. Wherever Name is needed you must use either a group or an alias. Wherever Target is needed you must use either an address or a Name (which is abstract, so you must
use either a group or an alias).
(More) Address Book Constraints
-
A Name is associated to a Target.
o
This needs further constraint since it would allow an alias to be associated to itself, e.g., Tom->Tom. This is undesirable. The next constraint rectifies this.
-
A Name cannot belong to the set of targets reachable from Name.
-
A Name mapped to more than one Target must be a group, not an alias.
-
An alias is mapped to one Target.
-
If you look up a name, you should get back an address (or multiple addresses if it’s a group). That is, the end of a naming chain must be an address (or multiple addresses if it is a group). For each name n, follow its naming chain to
the end and an address must be there. 1. There are 5 objects in an address book: Target, Name, Addr, Group, and Alias. 2. The objects are related in this way:
3. A Name is associated to a Target. (An
addr function maps Name to Target) 4. A Name may not reference itself. (In a naming chain no name may occur twice) 5. An alias may reference only one address.
6. Adding a new Name/Target pair to an address book: Let b be an address book. After adding to the address book the pair (n: Name, t: Target), the new address book is b’ where b’ = b union n->t. 7. Deleting a Name/Target pair from an address book: Let b be an address book. After deleting from the address book the pair (n: Name, t: Target), the new address book is b’ where b’ = b - n->t. 8. Delete undoes add: Let b be an address book. The address book after adding the pair (n: Name, t: Target) is b’. The address book after deleting the same pair is b’’. It must be that b = b’’. 9. Idempotent: Suppose a Name/Target pair is added to the address book. If the same Name/Target pair is added again, there is no change to the address book. 10. Suppose the name n’ is in the address book. Suppose the pair (n: Name, t: Target) is added to the address book, where n != n’. Adding n->t to the address book does not have any effect on
a lookup of n’ in the address book.
Address Book is a Satisfiability Problem Can an address book be created which satisfies all the constraints in the model? Are there counterexamples—instances that violate a property?
The address book problem is an instance of a satisfiability problem (SAT).
Because of recent advances in constraint-solving technology, the space of cases examined by a SAT tool is usually huge—billions of cases of more—and it therefore offers a degree of coverage unattainable
in testing. Alloy from MIT is a declarative specification language for expressing complex structural constraints and behavior in a software system, and a tool for exploring and checking properties of the
resulting structures. Cost: Free!
Alloy Representation of the Address Book Problem See the excellent book:
Software Abstractions Logic, Language Analysis by Daniel Jackson.
Relationship between Alloy and UML See this Stack Overflow post:
http://stackoverflow.com/questions/39182029/relationship-between-alloy-and-uml. Here’s an excerpt: UML diagrams aren’t expressive enough for detailed modeling. Also, see this paper:
Comparison of the Modeling Languages and Alloy. Here’s an excerpt: Both Alloy and UML can be used to specify the requirements Finally, see this paper:
Some Shortcomings of OCL, the Object Constraint Language of UML.
I am currently writing a tutorial on Alloy. [1] The description of the Email Address Book comes from Daniel Jackson’s book. Also, several other sentences in this article come from Jackson’s book. |
