Alloy is a formal language deeply rooted in Z. It was developed by Daniel Jackson, currently at MIT. Daniel is the son of Michael Jackson who is well-known for his contributions to computing. The Alloy analyzer is a constraint analyzer developed by Felix Chang, currently at MIT. Let us take the classic example of the address book and convert it into a formal equivalent model of a digital art gallery catalog. Here we are thinking of the names of paintings. A physical painting is located in exactly one place. But the digital form of that painting, which we will call digital image, may be located in many different places. Such digital images are to be subject to control, for quality purposes, for copyright purpose, and so on. To motivate the work we will concentrate on a real-world example: the digital art exhibition. But first let us start with the address book. In today's world we might be thinking of names and web addresses, or names and e-mail adresses, or ... There is so much potential. Let us be conservative and have some fun? Here is a simple old-fashioned address book: To build a model requires investment of time and energy. To develop a meaningful model of one's own helps to understand the process of model building. This gives one a sense of ownership in the model. One might experiment with the simple model above. For example, if interested in the prison system, one might change „Black Rock“ to „Black Rock penitentiary“ or „Black Rock jail“ and maybe change „on the road“ to „on the run“. Let us take the first first example used by Jackson in his book: module addressbook sig Name, Addr {} sig Book { addr: Name -> lone Addr } The special keyword lone needs explanation. It indicates that each name is mapped to at most one address. It is possible for someone to have no address. In our little model „Charlie Bigfoot“ has no address in the usual sense. So, just for fun, we have given him a special sort of address "on the road". We can get a picture of our simple model. The image on the left is the default layout in the Alloy analyzer; that on the right uses the „Magic Layout“. Our next step is to produce some typical address books. In particular we are interested to see if we can produce an example that corresponds to the old-fashioned address book with which we began. pred show () {} run show for 4 but 1 Book Following the pattern of Jackson's development closely, one adds the predicate show to get at most 4 objects in each signature: Name and Addr but only 1 object Book. So! We can think of „Harry Knooall“ having Name1, „Martha Underwude“ having Name0, „Black Rock, Big Peak county“ being represented by Addr2, and so on. In other words, we do have a good working model for the kind of address book we have in mind. Now what shall we do? Let us begin with a simple correspondence. An address book associates names with addresses. The exhibition catalog associates names of digital images (of paintings or whatever) with web addresses. We jump in straight away with the name of the module: module exhibitionCatalog The next step is the introduction of an abstract signature which we will call Xpoint. The idea behind Xpoint is to indicate some end point in an XML namespace. abstract sig Xpoint {} Now we can define exactly what we mean by the web address of the digital image (of the painting or whatever). sig WebAddr extends Xpoint {} We also consider the possibility of groups of names. The purpose of the group is to cover the concept of artistic theme, such as Impressionism, Cubism, and so on. Let us try out the use of ArtTheme for such a group? Similarly, an alias is a name for another name. It is frequently the case, that an artwork will have some name, such as Mother with Child. It is also possible that a caloguer will use an alias such as the Chicago Madonna for exactly the same artwork. It might seem convenient to use Alias for this purpose. However, in order to avoid confusion between this new (isomorphic) model and the original Jackson model we will use OtherName. Both ArtTheme and OtherName are sorts of Names, words which identify. But Name is used in the original Jackson model. Let us use instead the word Identity. And just as the Xpoint is in an XML space, then why not consider the Identity to be a kind of Xpoint? abstract sig Identity extends Xpoint {} Now we can define ArtTheme and OtherName as extensions of Identity: sig ArtTheme extends Identity {} sig OtherName extends Identity {} For convenience, one might like to wrap up the previous two defintion in one line: sig ArtTheme, OtherName extends Identity {} Finally the ArtExhibitionCatalog is determined by setting up a relationship between the Identity (of the ArtWork) and the Xpoint (where it is located). sig ArtExhibitionCatalog {webAddr: Identity —> Xpoint} Now we put everything together module exhibitionCatalog abstract sig Xpoint {} sig WebAddr extends Xpoint {} abstract sig Identity extends Xpoint {} sig ArtTheme, OtherName extends Identity {} sig ArtExhibitionCatalog {webAddr: Identity -> Xpoint} The first thing to do is show a picture of the structure of the metamodel: It might be a good idea to make a printout or a sketch of this picture while studying the rest of the model. Now we are ready to play with our little model. Before we do, it is really worthwhile to listen to what Daniel Jackson has to say on the subject: «Building a model incrementally with an analyzer, simulating and checking as you go along, is a very different experience from using pencil and paper alone. The first reaction tends to be amazement: modeling is much more fun when you get instant, visual feedback, When you simulate a partial model, you see examples immediately that suggest new constraints to be added.» The most basic way to show what is going on is to use the predicate show. Here we want to show some of the possible webAddresses associated with our ArtExhibitionCatalog: pred show (aec: ArtExhibitionCatalog) {some aec.webAddr} and we want to limit our exploration of the model to at most 3 objects in each signature, except for the ArtExhibitionCatalog which is limited to 1 object: run show for 3 but 1 ArtExhibitionCatalog Finally, to get a picture of what is happening with respect to the ArtExhibitionCatalog, we project over it. That is to say, we know there is just one. Let us put it in the background and see what the rest of the picture looks like. Here is one such result. We must go back and fix the model. Specifically, one might add the fact that for any ArtExhibitionCatalog there is no Identity that is in a set of Xpoints which can be reached from that Identity. In other words, cycling (i.e. going round in circles) is out! We state this as fact {     all aec: ArtExhibitionCatalog | no id: Identity | id in id.^(aec.webAddr)     } Now let us consider the following result: pred show (ace: ArtExhibitionCatalog) some OtherName. (ace.webaddress)} Starting again from the simple address book we can move in the direction of the vCard. The task is to find a simple way of building up the model of the vCard, step by step. Why not begin with the example given in the Wikipedia article? BEGIN:VCARD VERSION:2.1 N:Gump;Forrest FN:Forrest Gump ORG:Bubba Gump Shrimp Co. TITLE:Shrimp Man TEL;WORK;VOICE:(111) 555-1212 TEL;HOME;VOICE:(404) 555-1212 ADR;WORK:;;100 Waters Edge;Baytown;LA;30314;United States of America LABEL;WORK;ENCODING=QUOTED-PRINTABLE:100 Waters Edge=0D=0ABaytown, LA 30314=0D=0AUnited States of America ADR;HOME:;;42 Plantation St.;Baytown;LA;30314;United States of America LABEL;HOME;ENCODING=QUOTED-PRINTABLE:42 Plantation St.=0D=0ABaytown, LA 30314=0D=0AUnited States of America EMAIL;PREF;INTERNET:forrestgump@walladalla.com REV:20080424T195243Z END:VCARD Our first task is to identify the meaning of the "key" words which are apparently given in uppercase. We recognize TITLE, WORK, VOICE, HOME and so on. But what exactly is N, FN, REV? These "key" words are called properties. The basic list of properties is FN, N, NICKNAME, PHOTO, BDAY, ADR, LABEL, TEL, EMAIL, MAILER, TZ, GEO, TITLE, ROLE, LOGO, AGENT, ORG, CATEGORIES, NOTE, PRODID, REV, SORT-STRING, SOUND, URL, UID, VERSION, CLASS, KEY. Let us begin by organizing these in a nice table. We will not fill in all the details right now. http://www.imc.org/pdi/pdiproddev.html "Like Z, it describes all structures (in space and time) with a minimal toolkit of mathematical notions," Jackson 2006, p.xii Some brief information on Felix Chang is given in the e-Links. We use addressBook2 as the key example taken from Daniel Jackson's book Software Abstractions, p.17 In practical work we will use digital photographs as digital images in our exhibition. Such digital photographs will be freely available under the usual Creative Commons license. We have simplified Jackson's model a little bit. His module, page 6, has the longer title „tour/addressBook1“ It is important to be open about possible meanings of names. I say him. I could say her. If we want to be specific about gender, then we have to model it: female, male, other, for example. Jackson uses the name Target, p.17. It is very hard to imagine how one might come up with this particular way of doing things. In other words, to start with such an abstract signature seems to require prior knowledge. Such prior knowledge seems to require a great deal of sophistication or intuition. Jackson 2006, p.xiii vCard version 2.1 Specification vCard version 2.1 Specification vCard version 2.1 Specification vCard version 2.1 Specification Jackson, Daniel (2006). Software abstractions : logic, language and analysis. Cambridge, Massachusetts: The MIT Press. ISBN 978-0262101149. Felix Chang last access {2008-08-15} Representing vCard Objects in RDF/XML vCard, The Electronic Business Card, Version 2.1. A versit Consortium Specification, September 18, 1996
{'wiki_source': 'wikibooks', 'other_info': "{'content_model': 'wikitext', 'language': 'en', 'title': 'Modeling from A to Z/Modeling principles/A is for Alloy analyzer', 'type': 'text'}"}