{"id":1515,"date":"2011-09-24T11:32:36","date_gmt":"2011-09-24T15:32:36","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/?p=1515"},"modified":"2011-09-24T11:32:36","modified_gmt":"2011-09-24T15:32:36","slug":"a-taste-of-specification-with-alloy","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2011\/09\/24\/a-taste-of-specification-with-alloy\/","title":{"rendered":"A Taste of Specification with Alloy"},"content":{"rendered":"

In my last post (which was, alas, a stupidly long time ago!), I talked a bit about software specification, and promised to talk about my favorite dedicated specification tool, Alloy. Alloy is a very cool system, designed at MIT by Daniel Jackson and his students.<\/p>\n

Alloy is a language for specification, along with an environment which allows you to test your specifications. In a lot of ways, it looks like a programming language – but it’s not<\/em>. You can’t<\/em> write programs in Alloy. What you can do is write concise, clear, and specific descriptions<\/em> of how something else works.<\/p>\n

I’m not going to try to really teach you Alloy. All that I’m going to do is give you a quick walk-though, to try to show you why it’s worth the trouble of learning. If you want to learn it, the Alloy group’s website has a really good the official Alloy tutorial<\/a>. which you should walk through.<\/p>\n

<\/p>\n

We’ll walk through Alloy using a canonical example, most of which is taken from the tutorial – a filesystem. Program specification tools are constantly described using a filesystem, because it makes a great example. The basic concepts of filesystems are familiar to just about everyone.They’re complex enough to be interesting, but simple enough to be tractable. On a personal note, I really like this example, because the filesystem model is also closely related to the example that motivated me to first try Alloy out.<\/p>\n

Alloy is based, ultimately, on set theory. It provides you with a very constrained way of talking about things in terms of sets. It can be a bit tricky at times: many typical Alloy statements sort-of look like they’re statements in a normal programming language that are performing operations on objects. But they’re not. They’re expressions describing sets<\/em> and relationships between sets. It’s important to always keep that in mind when you’re reading Alloy specifications.<\/p>\n

The most basic element of a spec in Alloy is a signature. A signature defines a set of atoms<\/em> and a collection of properties that exist for those objects. A signature is almost like a class in an object-oriented programming language – but that’s really because the object-oriented notion is based on set theory, rather than Alloy specifications being object-oriented per se.<\/p>\n

Here’s a basic definition of file system objects in Alloy:<\/p>\n

\nsig FSObject { parent : lone Dir }\nsig Dir extends FSObject {\n\tchildren: set FSObject\n}\n\nsig FileContents { }\n\nsig File extends FSObject {\n\t contents: one FileContents\n}\n\n<\/pre>\n
 This says that there’s a set<\/em> of objects that we call filesystem objects. Every filesystem object has a property, “parent”, and a filesystem object’s parent can be either 0 or 1 other filesystem objects.<\/p>\n
 To harp on a point: the definition of parent<\/code> looks like it defines a field of a class. It doesn’t. It defines a relation<\/em> between atoms. Taken together with the signature definition that encloses it, it asserts that there is a set of objects, which we’re calling FSOBject<\/code>; and for each filesystem object in that set, there’s a predicate<\/em> that can associate it with another FSObject<\/code>. In alloy, you are not<\/em> defining objects. You can’t “create” a filesystem object with a particular parent. You can just assert that filesystem objects exist, and that they are related to other objects that we call their parents. <\/p>\n
 After the base FSObject<\/code> set is defined, we can define subsets of it. We define two: the Dir<\/code> objects also have a children<\/code> property; and the File<\/code> object, which has contents. We don’t care what the contents of a file are – we’re not going to talk about the properties of the contents of the file. We say that by giving them an empty declaration. <\/p>\n
 Once we’ve defined objects, we can describe the way they behave by using facts. A fact is an assertion – something that we assert must always be true. For example:<\/p>\n
\n  fact { all d: Dir, o: d.children | o.parent = d }\n\n<\/pre>\n
 This says that for any directory d<\/code>, if a file o<\/code> is in the children of d<\/code>, then the parent of o<\/code> must be d<\/code>. So we’ve just stated a really important property of our filesystem. It’s not<\/em> like a Unix filesystem: in Unix, a file can be a member of many directories; in our model filesystem, we’ve said that it can’t. That’s the kind of thing that really matters, and that a specification helps you clarify. If you don’t think about that, you can make some really dreadful errors in your filesystem by sometimes assuming that a file can’t be in more than one directory! Even at this ridiculously simple level, there’s already a potential benefit to this specification stuff. (This used to contain an error; I copied an earlier version of the assertion, where I had used the name “contents” for both the relation between a directory and its children, and the relation between a file and its contents object. Thanks to reader Paul Batum for catching it!)<\/em><\/p>\n
 Now, we can move on to more facts:<\/p>\n
\none sig Root extends Dir { } { no parent }\n\nfact { FSObject in Root.*contents }\n\n<\/pre>\n
 The first of these uses an alternative way of handling facts. You can state a fact about a sig<\/code> by putting a second brace-block after the signature – each line in that is a fact that’s true for all members of the set. The fact “no parent<\/code>” is Alloy’s notation for saying that a relation is empty – it’s equivalent to something like forall x : FSObject | x notin Root.parent, or cardinality(Root.parent) = 0<\/code>. So what this says is that there’s exacty one special directory, called the Root<\/code>, which has no parent. Taken together, this facts and the “one<\/code>” annotation mean that there is only one root – we’re saying that the subset of Dir<\/code> that has no parent contains exactly one element. <\/p>\n
 The second fact, in the more typical fact form, says that the filesystem is completely connected. Root.*contents<\/code> is equivalent to Root.contents<\/code> unioned with Root.contents.contents<\/code>, unioned with Root.contents.contents.contents<\/code>. In other words, it’s the transitive closure of the elements of the contents<\/code> relation.<\/p>\n
 So now we have a basic Alloy specification that describes one of the salient characteristics of a filesystem. What have we gained by doing this?  One of the things that makes Alloy particularly amazing as a specification tool is that it isn’t just static. When you give it a specification, you can also make statements that you believe should<\/em> be true. Alloy can then check to see if they are<\/em> in fact true; and if they aren’t, it can generate a specific counterexample. So if you’re wrong, Alloy doesn’t just tell you you’re wrong: it shows you a specific example demonstrating why<\/em>.<\/p>\n
 Let’s try an example of that. Suppose we accidentally forgot use the “one” annotation on root. But one of the key properties of a filesystem is that it only has one root. So we could write an assertion:<\/p>\n
\n\/\/ File system has one root\nassert oneRoot { one d: Dir | no d.parent }\ncheck oneRoot for 5\n\n<\/pre>\n
 This says that we believe that there should be only one directory which has no parent – that is, that there is one root. Then we tell it to check that for a scope of 5. That means that we want it to try to build instances where there are 5 distinct instances of each signature. In general, you can’t compute examples for large scopes; but again, speaking in general, that’s not a problem. Most of the time, when you’ve got an error in the spec, it doesn’t take that many objects to reveal it.<\/p>\n
 Let’s give it a shot here. When I plug this into Alloy, I get several counterexamples. The most obvious is this one:<\/p>\n
\"\"<\/a><\/p>\n
 It’s got three directories, two of which are roots. That’s a nice minimal counter-example. It’s not surprising; that’s exactly what I had in mind when I initially removed the “one” from the declaration of “Root”.  But it also produces another counterexample, which surprised me.<\/p>\n
 My specification, as written, also permits a case where there are no<\/em> root directories; in fact, there are no files<\/em>, but there are some “FileContents” not associated with files. For this latter example, in the specification, I forgot to say that a file-contents must be associated with a file. I can correct this by adding a fact:<\/p>\n
\nfact { all fc : FileContents | some f : File | f.contents = fc }\n\n<\/pre>\n
 This says that all filecontents are associated with files. The way that I wrote it, it allows multiple files to share the same contents. To write that, I needed to decide just what I wanted them to mean. The contents could<\/em> be something like the chunk of data on disk that’s stored in the file. If that were the case, then for a simple filesystem, there should be a one-to-one relationship between files and contents. On the other hand, if the contents of a file were the data stored in the file, then there’s no reason that two different files wouldn’t have the same contents. <\/p>\n
 This kind of decision process is very typical of the process of specification. Specification is about finding the places where your understanding of the system that you’re building is incomplete – exactly the way that Alloy just helped us here.<\/p>\n
 With that fixed, and the “one” added back to the root declaration, Alloy finds no counterexamples. My specification is correct, at least within the scope size that I tested.<\/p>\n
 The specification so far is completely static. It doesn’t allow for any concept of time or change. But a real filesystem does change. You can create files, delete files, move files, etc. To do that in allow, you use predicates. Predicates are, roughly, the Alloy equivalent of functions. A predicate lets you abstract a collection of facts over a set of parameters. For example, we could write a predicate that tests if an FSObject<\/code> is a child of a particular directory:<\/p>\n
\npred IsChild[f : FSObject, d : Dir] {\n   f in d.*children\n}\n\n<\/pre>\n
 The way that we capture time in Alloy is to talk about the states of an object before and after an operation. Before I get to that, I’m going to introduce a variation of the filesystem specification. The original spec just said that there was one root directory in the universe. But now, that’s not going to work – because we need to be able to talk about the root directory both before and after<\/em> some operation, and we’re going to talk about them as two different objects<\/em>. So we need to have a notion of a filesystem as an object itself – then, we can have multiple filesystems, each of which has exactly one root directory.<\/p>\n
\n\/\/ File system objects\nabstract sig FSObject { }\nsig File, Dir extends FSObject { }\n\n\/\/ A File System\nsig FileSystem {\n  live: set FSObject,\n  root: Dir & live,\n  parent: (live - root) ->one (Dir &live),\n  contents: Dir -> FSObject\n}{\n  \/\/ live objects are reachable from the root\n  live in root.*contents\n  \/\/ parent is the inverse of contents\n  parent = ~contents\n}\n\n<\/pre>\n
 So, we now have a filesystem object. The directory-containment relationship is now not part of the individual directories, but it’s part of the filesystem object itself. So when we change the filesystem, we only need to change the state of that one object.<\/p>\n
 The way that we do that is by saying that the “parent” relation is a mapping from each member of the set of live filesystem objects excluding the root<\/em> to exactly one live directory in the filesystem. Then in the facts for the signature, we also say the parent relation and the contents relation are inverses – so when we later describe a change in either one, the other is automatically updated to match. This illustrates one of the nice things about specification: we never have to say how<\/em> to do something. A specification isn’t about how<\/em>; it’s about what. So we need to say what the effect of an operation is, but unless we want to, we don’t need to say how it’s performed.<\/p>\n
 Now, within this, we can write a “move” operation, to move a file from one directory to another:<\/p>\n
\npred move [fs, fs': FileSystem, x: FSObject, d: Dir] {\n  (x + d) in fs.live\n  fs'.parent = fs.parent - x->(x.(fs.parent)) + x->d\n}\n\n<\/pre>\n
 “fs” is the state of the filesystem before the operation; “fs'” is the state of the filesystem after.  So this predicate says that “I successfully moved x to d in fs resulting in fs’ if and only if the following facts are true:”<\/p>\n
    \n
  1.  Both the file and the target directory are part of the filesystem.<\/li>\n
  2.  The parent relation in “fs'” has the old relationship for x removed (so that x was removed from its old directory), and the new parentage of “x” added (so that it’s now a child of the target directory).<\/li>\n<\/ol>\n
     Again, we’re exploiting the fact that we don’t need to say how<\/em> move works – we’re just saying what it does.<\/p>\n
     There’s a whole lot more to Alloy. I don’t want to go into more detail here, because I don’t think I can do it justice. Alloy is an amazing tool, but it’s not a simple one. The last time that I did serious work in Alloy was in Alloy version 3 (I think; it might even have been v2). In the transition from to the current version, the language has changed dramatically for the better – but I spent nearly enough time learning the new version. If enough readers are interested, I’ll spend some time re-building my old SCM specification in Alloy4, and then write a series of posts about it.<\/p>\n","protected":false},"excerpt":{"rendered":"
    In my last post (which was, alas, a stupidly long time ago!), I talked a bit about software specification, and promised to talk about my favorite dedicated specification tool, Alloy. Alloy is a very cool system, designed at MIT by Daniel Jackson and his students. Alloy is a language for specification, along with an environment […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[93,54],"tags":[100,313,235],"class_list":["post-1515","post","type-post","status-publish","format-standard","hentry","category-program-specification","category-programming","tag-alloy","tag-programming","tag-specification"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-or","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1515","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=1515"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/1515\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=1515"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=1515"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=1515"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}