Create better models, better data specifications, and better softwarespe

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]

Address Book, Example #1

Address Book, Example #2

Only One Place to Change when an Address Changes

Sets and Set Relations

The set of addresses:

               {tom@foo.com, sara@f..., bill@f..., lynn@f...}

The set of aliases:

               {Tom, Sara, Bill, Lynn}

The set of groups:

               {Department-A, Department-B, Friends}

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

Instance, State, State Space

Earlier we saw this instance:

That is one possible state of an address book. The set of all possible states is the state space.

Address Book Constraints

-          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

Generalize the Concepts

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.

Classification Hierarchy

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.

Model of an Address Book

1. There are 5 objects in an address book: Target, Name, Addr, Group, and Alias.

2. The objects are related in this way:

• Target is abstract.
• Name is abstract.
• Addr and Name extend Target.
• Group and Alias extend Name.

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

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.
               The UML constraint language OCL does cover the same kinds of
               details as Alloy but does not have the automated support to the
               same degree.

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
               to design complex software systems. The syntax of Alloy is
               largely compatible with UML. UML is more complicated, while
               Alloy is more abstract. It is promising that part of UML can be
               formalized and transmitted to Alloy to allow automatic model
               validation analyzing in order to reduce errors in the requirement
               and design stages.

Finally, see this paper: Some Shortcomings of OCL, the Object Constraint Language of UML.

Tutorial on Alloy

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.