--- /dev/null
+@title:A Micromodularity Mechanism\r
+@section:1 Testing\r
+@noindent:This is gamma: <f"Symbol"><\#103><f$>.<\n> This is Delta: <f"Symbol"><\#68><f$>.<\n> This is oplus: . <f"LucidNewMatSymT"><\#65><f$> <f"Symbol"><\#222><f$> <f"LucidNewMatSymT"><\#65><f$>\r
+@body:This is a subscripted variable: A<-><B>hello<B>there<->. Math mode: <I>x<I> + 2 = <I>y<I>, <I>and<I> && <I>x<I><->2<-> = <I>y<I><->3<-> = <I>x<I><-><I>ijk<I><->\r
+@author:Daniel Jackson, Ilya Shlyakhter and Manu Sridharan<\n> Laboratory for Computer Science<\n> Massachusetts Institute of Technology<\n> Cambridge, Massachusetts, USA<\n> dnj@mit.edu\r
+@opening:Abstract\r
+@noindent:A simple mechanism for structuring specifications is described. By modelling structures as atoms, it remains entirely first<\#45>order and thus amenable to automatic analysis. And by interpreting fields of structures as relations, it allows the same relational operators used in the formula language to be used for dereferencing. An extension feature allows structures to be developed incrementally, but requires no textual inclusion nor any notion of subtyping. The paper demonstrates the flexibility of the mechanism by application in a variety of common idioms.\r
+@subsection:1.1 Categories and Subject Descriptors\r
+@noindent:D.2.1 Requirements/Specifications<\#151>Languages; D.2.4 Software/Program Verification<\#151>Formal methods, Model checking; F.3.1 Specifying and Verifying and Reasoning about Programs<\#151>Assertions, Invariants, Specification techniques.\r
+@subsection:1.2 General Terms\r
+@noindent:Design; Documentation; Languages; Verification.\r
+@subsection:1.3 Keywords\r
+@noindent:Modeling languages; formal specification; first<\#45>order logic; relational calculus; Alloy language; Z specification language; schema calculus.\r
+@section:2 Introduction\r
+@noindent: I am neither crazy nor a micromaniac.<\n> (A micromaniac is someone obsessed with<\n> reducing things to their smallest possible form.<\n> This word, by the way, is not in the dictionary.)<\n> <\#150><I>Edouard de Pomiane, French Cooking in Ten Minutes, 1930<I>\r
+@noindent:Most specification languages provide mechanisms that allow larger specifications to be built from smaller ones. These mechanisms are often the most complicated part of the language, and present obstacles to analysis. This paper presents a simple mechanism that seems to be expressive enough for a wide variety of uses, without compromising analyzability.\r
+@body:This work is part of a larger project investigating the design of a <\#147>micro modelling language<\#148>. Our premise is that lightweight application of formal methods [6] demands an unusually small and simple language that is amenable to fully automatic semantic analysis. The Alloy language is the result to date of our efforts to design such a language. Based on our experiences with the language [4] and its analyzer [5], we have recently developed a revision of Alloy that overcomes many of its limitations. This paper describes the key feature of the revised language: the <I>signature<I>, a new modularity mechanism.\r
+@body:The mechanism allows our existing analysis scheme [3] to be applied to specifications involving structures. This is not achieved by treating the structuring mechanism as a syntactic sugar, which would limit the power of the notation (ruling out, for example, quantification over structures) and would complicate the analysis tool and make output harder for users to interpret. Because of the mechanism<\#48>s generality, it has also enabled us to simplify the language as a whole, making it more uniform and eliminating some ad hoc elements.\r
+@body:Our mechanism has a variety of applications. It can express inherent structure in the system being modelled, and can be used to organize a specification in which details are added incrementally. It can be used to construct a library of datatypes, or to describe a system as an instantiation of a more general system. And it can express state invariants, transitions, and sequences, despite the lack of any special syntax for state machines.\r
+@body:In this last respect, the new language differs most markedly from its predecessor [4], which provided built<\#45>in notions of state invariants and operations. We now think this was a bad idea, because it made the language cumbersome for problems (such as the analysis of security policies or architectural topology constraints) in which temporal behaviour can be fruitfully ignored, and too inflexible for many problems in which temporal behaviour is important.\r
+@body:Our paper begins by explaining our motivations<\#151>the requirements our mechanism is designed to meet. The mechanism is then presented first informally in a series of examples, and then slightly more rigorously feature<\#45>by<\#45>feature. We discuss related work, especially the schema calculus of Z, and close with a summary of the merits and deficiences of our notation as a whole.\r
+@section:3 Requirements\r
+@noindent:The goal of this work was to find a single structuring mechanism that would support a variety of common specification idioms:\r
+@point:\alpha 3.0.A <I>States<I>: description of complex state as a collection of named components; incremental description both by hierarchy, in which a complex state becomes a component of a larger state, and by extension, in which new components are added; declaration of invariants and definitions of derived components;\r
+@point:\alpha 3.0.B <I>Datatypes<I>: separate description of a library of polymorphic datatypes, such as lists, sequences, trees and orders, along with their operators;\r
+@point:\alpha 3.0.C <I>Transitions<I>: specification of state transitions as operations described implicitly as formulas relating pre<\#45> and post<\#45>state; composition of operations from previously defined invariants and operations; sequential composition of operations; description of traces as sequences of states;\r
+@point:\alpha 3.0.D <I>Abstractions<I>: description of abstraction relations between state spaces;\r
+@point:\alpha 3.0.E <I>Assertions<I>: expression of properties intended to be redundant, to be checked by analysis, including: relationships amongst invariants; wellformedness of definitions (eg, that an implicit definition is functional); establishment and preservation of invariants by operations; properties of states reachable along finite traces; and simulation relationships between abstract and concrete versions of an operation.\r
+@noindent:We wanted additionally to meet some more general criteria:\r
+@point:\alpha 3.0.F <I>Simplicity<I>. The language as a whole should be exceptionally small and simple.\r
+@point:\alpha 3.0.G <I>Flexibility<I>. Support for the particular idioms of state<\#45>machine specification should not be a straitjacket; the language should not dictate how state machines are expressed, and should not make it hard to describe structures that are not state machines (such as security models and architectural styles).\r
+@point:\alpha 3.0.H <I>Analyzability<I>. A fully automatic semantic analysis should be possible. In the present work, this has been achieved by requiring that the modularity mechanism be first order, and expressible in the kernel of the existing language.\r
+@noindent:Finally, our language design decisions have been influenced by some principles that we believe contribute to these goals, make the language easier to use, and analysis tools easier to build:\r
+@point:\alpha 3.0.I <I>Explicitness<I>. The language should be fully explicit, with as few implicit constraints, coercions, etc, as possible.\r
+@point:\alpha 3.0.J <I>Minimal mathematics<I>. The basic theory of sets and relations should suffice; it should not be necessary to introduce domains, fixed points, infinities or special logical values.\r
+@point:\alpha 3.0.K <I>Minimal syntax<I>. There should be very few keywords or special symbols, and no need for special typography or layout.\r
+@point:\alpha 3.0.L <I>Uniformity<I>. A small and general set of constructs should be applied uniformly, independent of context.\r
+@point:\alpha 3.0.M <I>Lack of novelty<I>. Whenever possible, notions and syntax should follow standard usage of conventional mathematics and programming.\r
+@section:4 Informal Description\r
+@noindent:As a running example, we will specify a simple memory system involving a cache and a main memory. The memory has a fixed set of addresses and associates a data value with each address. The cache, in contrast, associates data values with some subset of addresses that varies over time. The cache is updated by a <\#147>write<\#45>back scheme<\#148>, which means that updates need not be reflected to main memory immediately. The cache may therefore hold a more current value for an address than the main memory; the two are brought into alignment when the address is flushed from the cache and its value is written to main memory.\r
+@subsection:4.1 States\r
+@noindent:We start by declaring the existence of addresses and data values:\r
+@geekmath:sig Addr {}<\n> sig Data {}\r
+@noindent:Each line declares a <I>signature<I>, and introduces a set of atoms: <I>Addr<I> for the set of addresses, and <I>Data<I> for the set of data values. Like <\#145>given types<\#146> in Z, these sets are disjoint from one another, and their atoms are unstructured and uninterpreted. Signature names can be used as expressions denoting sets, but they are also treated as types, so the expression <I>Addr+Data<I>, for example, is ill<\#45>typed, since the union operator (+) requires the types of its operands to match.\r
+@body:The signature declaration\r
+@geekmath:sig Memory {<\n> addrs: set Addr,<\n> map: addrs <\#45>! Data<\n> }\r
+@noindent:likewise declares a set of atoms, <I>Memory<I>, corresponding to the set of all possible memories. In addition, it declares two fields: <I>addrs<I> and <I>map<I> which associate with a memory a set of addresses and a mapping from addresses to data values respectively. Thus, given a memory <I>m<I>, the expression <I>m.addrs<I> will be a set of addresses, <I>m.map<I> will be a relation from addresses to data values. The memory, addresses and data values should be viewed as distinct atoms in their own right; fields don<\#48>t decompose an atom, but rather relate one atom to others. The exclamation mark in the declaration of the field <I>map<I> is a <\#145>multiplicity marking<\#146>: it says that <I>m.map<I> associates exactly one data value with each address in the set <I>m.addrs<I>. The use of <I>addrs<I> rather than <I>Addr<I> on the left side of the arrow indicates that <I>m.map<I> does not associate a data value with an address that is not in the set <I>m.addrs<I>.\r
+@body:In these expressions, the dot is simply relational image. More precisely, when we say that <I>m<I> is a memory, we mean that the expression <I>m<I> denotes a set consisting of a single atom. The field <I>addrs<I> is a relation from <I>Memory<I> to <I>Addr<I>, and <I>m.addrs<I> denotes the image of the singleton set under this relation. So for a set of memories <I>ms<I>, the expression <I>ms.addrs<I> will denote the union of the sets of addresses that belong to the individual memories. Given an address <I>a<I>, the expression <I>a.(m.map)<I> denotes the set of data values associated with address <I>a<I> in memory <I>m<I>, which will either be empty (when the address is not mapped) or a singleton. For convenience, we allow the relational image <I>s.r<I> to be written equivalently as <I>r<I>[<I>s<I>], where [] binds more loosely than dot, so this expression may be written as <I>m.map<I>[<I>a<I>] instead.\r
+@body:Like objects of an object<\#45>oriented language, two distinct atoms can have fields of the same value. Unlike objects, however, atoms are immutable. Each field is fixed, and cannot map an atom to one value at one time and another value at another time. To describe an operation that changes the state of a memory, therefore, we will use two distinct atoms in the set <I>Memory<I> to represent the memory<\#48>s state before and after.\r
+@subsection:4.2 Extension\r
+@noindent:A signature declaration can introduce a set as a subset of one previously declared, in which case we call it a <I>subsignature<I>. In this case, the set does not correspond to a type, but rather its atoms take on the type of the superset. For example, the declaration\r
+@geekmath:sig MainMemory extends Memory {}\r
+@noindent:introduces a set of atoms <I>MainMemory<I> representing main memories, which is constrained to be a subset of the set <I>Memory<I>. Likewise\r
+@geekmath:sig Cache extends Memory {<\n> dirty: set addrs<\n> }\r
+@noindent:introduces a set of atoms <I>Cache<I> representing those memories that can be regarded as caches. It also introduces a field <I>dirty<I> that associates with a cache the set of addresses that is dirty; later, we will use this to represent those addresses for which a cache and main memory differ. Because <I>Cache<I> is a subset of <I>Memory<I>, and <I>m.addrs<I> (for any memory <I>m<I>) is a subset of <I>Addr<I>, the field denotes a relation whose type is from <I>Memory<I> to <I>Addr<I>. Expressions such as <I>m.dirty<I> are therefore type<\#45>correct for a memory <I>m<I>, whether or not <I>m<I> is a cache. But since declaration of the field <I>dirty<I> within the signature <I>Cache<I> constrains <I>dirty<I> to be a relation that maps only caches, <I>m.dirty<I> will always denote the empty set when <I>m<I> is not a cache.\r
+@body:This approach avoids introducing a notion of subtyping. Subtypes complicate the language, and tend to make it more difficult to use. In OCL [17], which models extension with subtypes rather than subsets, an expression such as <I>m.dirty<I> would be illegal, and would require a coercion of <I>m<I> to the subtype <I>Cache<I>. Coercions do not fit smoothly into the relational framework; they interfere with the ability to take the image of a set under a relation, for example. Moreover, subtypes are generally disjoint, whereas our approach allows the sets denoted by subsignatures to overlap. In this case, we<\#48>ll add a constraint (in Section 2.4 below) to ensure that <I>MainMemory<I> and <I>Cache<I> are in fact disjoint.\r
+@body:Declaring <I>Cache<I> and <I>MainMemory<I> as subsignatures of <I>Memory<I> serves to factor out their common properties. Extension can be used for a different purpose, in which a single signature is developed by repeated extensions along a chain. In this case, the supersignatures may not correspond to entities in the domain being modelled, but are simply artifacts of specification<\#151>fragments developed along the way. Z specifications are typically developed in this style.\r
+@subsection:4.3 Hierarchy\r
+@noindent:The signature declaration also supports hierarchical structuring. We can declare a signature for systems each consisting of a cache and a main memory:\r
+@geekmath:sig System {<\n> cache: Cache,<\n> main: MainMemory<\n> }\r
+@noindent:Again, <I>System<I> introduces a set of atoms, and each field represents a relation. The omission of the keyword <I>set<I> indicates that a relation is a total function. So for a system <I>s<I>, the expression <I>s.cache<I> denotes one cache<\#151>that is, a set consisting of a single cache. This is one of very few instances of implicit constraints in our language, which we introduced in order to make declaration syntax conventional.\r
+@body:Since signatures denote sets of atoms, apparently circular references are allowed. Linked lists, for example, may be modelled like this, exactly as they might be implemented in a language like Java:\r
+@geekmath:sig List {}<\n> sig NonEmptyList extends List {elt: Elt, rest: List} There is no recursion here; the field <I>rest<I> is simply a homogeneous relation of type <I>List<I> to <I>List<I>, with its domain restricted to the subset <I>NonEmptyList<I>.\r
+@subsection:4.4 State Properties\r
+@noindent:Properties of signature atoms are recorded as logical formulas. To indicate that such a property always holds, we package it as a <I>fact<I>. To say that, for any memory system, the addresses in a cache are always addresses within the main memory, we might write:\r
+@geekmath:fact {all s: System | s.cache.addrs in s.main.addrs}\r
+@noindent:or, using a shorthand that allows facts about atoms of a signature to be appended to it:\r
+@geekmath:sig System {cache: Cache, main: MainMemory}<\n> {cache.addrs in main.addrs}\r
+@noindent:The appended fact is implicitly prefixed by\r
+@geekmath:all this: System | with this |\r
+@noindent:in which the <I>with<I> construct, explained in Sectiom 3.6 below, causes the fields implicitly to be dereferences of the atom <I>this<I>.\r
+@body:A fact can constrain atoms of arbitrary signatures; to say that no main memory is a cache we might write:\r
+@geekmath:fact {no (MainMemory & Cache)}\r
+@noindent:where <I>no e<I> means that the expression <I>e<I> has no elements, and & is intersection.\r
+@body:Most descriptions have more interesting facts. We can express the fact that linked lists are acyclic, for example:\r
+@geekmath:fact {no p: List | p in p. @sep rest}\r
+@noindent:The expression <I> @sep rest<I> denotes the transitive closure of the relation <I>rest<I>, so that <I>p.^rest<I> denotes the set of lists reachable from <I>p<I> by following the field <I>rest<I> once or more. This illustrates a benefit of treating a field as a relation<\#151>that we can apply standard relational operators to it<\#151>and is also an example of an expression hard to write in a language that treats extension as subtyping (since each application of <I>rest<I> would require its own coercion).\r
+@body:Often we want to define a property without imposing it as a permanent constraint. In that case, we declare it as a <I>function<I>. Here, for example, is the invariant that the cache lines not marked as dirty are consistent with main memory:\r
+@geekmath:fun DirtyInv (s: System) {<\n> all a !: s.cache.dirty | s.cache.map[a] = s.main.map[a]<\n> } (The exclamation mark negates an operator, so the quantification is over all addresses that are <I>not<I> dirty.) Packaging this as a function that can be applied to a particular system, rather than as a fact for all systems, will allow us to express assertions about preservation of the invariant (Section 2.8).\r
+@noindent:By default, a function returns a boolean value<\#151>the value of the formula in its body. The value of <I>DirtyInv(s)<I> for a system <I>s<I> is therefore true or false. A function may return non<\#45>boolean values. We might, for example, define the set of bad addresses to be those for which the cache and main memory differ:\r
+@geekmath:fun BadAddrs (s: System): set Addr {<\n> result = {a: Addr | s.cache.map[a] != s.main.map[a]}<\n> }\r
+@noindent:and then write our invariant like this:\r
+@geekmath:fun DirtyInv (s: System) {BadAddrs(s) in s.cache.dirty}\r
+@noindent:In this case, <I>BadAddrs(s)<I> denotes a set of addresses, and is short for the expression on the right<\#45>hand side of the equality in the definition of the function <I>BadAddrs<I>. The use of the function application as an expression does not in fact depend on the function being defined explicitly. Had we written\r
+@geekmath:fun BadAddrs (s: System): set Addr {<\n> all a: Addr | a in result iff s.cache.map[a] != s.main.map[a]<\n> } the application would still be legal; details are explained in Section 3.7. \r
+@subsection:4.5 Operations\r
+@noindent:Following Z, we can specify operations as formulas that constrain pre<\#45> and post<\#45>states. An operation may be packaged as a single function (or as two functions if we want to separate pre<\#45> and post<\#45>conditions in the style of VDM or Larch).\r
+@body:The action of writing a data value to an address in memory might be specified like this:\r
+@geekmath:fun Write (m,m<\#48>: Memory, d: Data, a: Addr) {<\n> m<\#48>.map = m.map ++ (a<\#45>d)<\n> }\r
+@noindent:The formula in the body of the function relates <I>m<I>, the value of the memory before, to <I>m<\#48><I>, the value after. These identifers are just formal arguments, so the choice of names is not significant. Moreover, the prime mark plays no special role akin to decoration in Z<\#151>it<\#48>s a character like any other. The operator ++ is relational override, and the arrow forms a cross product. As mentioned above, scalars are represented as singleton sets, so there is no distinction between a tuple and a relation. The arrows in the expressions <I>a<\#45><I>d here and <I>addrs<\#45><I>Data in the declaration of the <I>map<I> field of <I>Memory<I> are one and the same. The action of reading a data value can likewise be specified as a function, although since it has no side<\#45>effect we omit the <I>m<\#48><I> parameter:\r
+@geekmath:fun Read (m: Memory, d: Data, a: Addr) {<\n> d = m.map[a]<\n> } Actions on the system as a whole can be specified using these primitive operations; in Z, this idiom is called <\#145>promotion<\#146>. A read on the system is equivalent to reading the cache:\r
+@geekmath:fun SystemRead (s: System, d: Data, a: Addr) {<\n> Read (s.cache, d, a)<\n> }\r
+@noindent:The <I>Read<I> operation has an implicit precondition. Since the data parameter <I>d<I> is constrained (implicitly by its declaration) to be scalar<\#151>that is, a singleton set<\#151>the relation <I>m.map<I> must include a mapping for the address parameter <I>a<I>, since otherwise the expression <I>m.map[a]<I> will evaluate to the empty set, and the formula will not be satisfiable. This precondition is inherited by <I>SystemRead<I>. If the address <I>a<I> is not in the cache, the operation cannot proceed, and it will be necessary first to load the data from main memory. It is convenient to specify this action as a distinct operation:\r
+@geekmath:fun Load (s,s<\#48>: System, a: Addr) {<\n> a !in s.cache.addrs<\n> s<\#48>.cache.map = s.cache.map + (a<\#45>s.main.map[a])<\n> s<\#48>.main = s.main<\n> }\r
+@noindent:The + operator is just set union (in this case, of two binary relations, the second consisting of a single tuple). A write on the system involves a write to the cache, and setting the dirty bit. Again, this can be specified using a primitive memory operation:\r
+@geekmath:fun SystemWrite (s,s<\#48>: System, d: Data, a: Addr) {<\n> Write (s.cache, s<\#48>.cache, d, a)<\n> s<\#48>.cache.dirty = s.cache.dirty + a<\n> s<\#48>.main = s.main<\n> }\r
+@noindent:A cache has much smaller capacity than main memory, so it will occasionally be necessary (prior to loading or writing) to flush lines from the cache back to main memory. We specify flushing as a non<\#45>deterministic operation that picks some subset of the cache addrs and writes them back to main memory:\r
+@geekmath:fun Flush (s,s<\#48>: System) {<\n> some x: set s.cache.addrs {<\n> s<\#48>.cache.map = s<\#48>.cache.map <\#45> (x<\#45>Data)<\n> s<\#48>.cache.dirty = s.cache.dirty <\#45> x<\n> s<\#48>.main.map = s.main.map ++ <\n> {a: x, d: Data | d = s.cache.map[a]}<\n> }\r
+@noindent:The <\#45> operator is set difference; note that it is applied to sets of addresses (in the third line) and to binary relations (in the second). The comprehension expression creates a relation of pairs <I>a<I><\#45><I>d<I> satisfying the condition.\r
+@body:Finally, it is often useful to specify the initial conditions of a system. To say that the cache initially has no addresses, we might write a function imposing this condition on a memory system:\r
+@geekmath:fun Init (s: System) {no s.cache.addrs}\r
+@subsection:4.6 Traces\r
+@noindent:To support analyses of behaviours consisting of sequences of states, we declare two signatures, for ticks of a clock and traces of states:\r
+@geekmath:sig Tick {}<\n> sig SystemTrace {<\n> ticks: set Tick,<\n> first, last: ticks,<\n> next: (ticks <\#45> last) !<\#45>! (ticks <\#45> first)<\n> state: ticks <\#45>! System}<\n> {<\n> first.*next = ticks<\n> Init (first.state)<\n> all t: ticks <\#45> last | <\n> some s = t.state, s<\#48> = t.next.state |<\n> Flush (s,s<\#48>)<\n> || (some a: Addr | Load (s,s<\#48>,a))<\n> || (some d: Data, a: Addr | SystemWrite (s,s<\#48>,d,a))<\n> }\r
+@noindent:Each trace consists of a set of <I>ticks<I>, a <I>first<I> and <I>last<I> tick, an ordering relation <I>next<I> (whose declaration makes it a bijection from all ticks except the last to all ticks except the first), and a relation <I>state<I> that maps each tick to a system state.\r
+@body:The fact appended to the signature states first a generic property of traces: that the ticks of a trace are those reachable from the first tick. It then imposes the constraints of the operations on the states in the trace. The initial condition is required to hold in the first state. Any subsequent pair of states is constrained to be related by one of the three side<\#45>effecting operations. The existential quantifier plays the role of a <I>let<I> binding, allowing <I>s<I> and <I>s<\#48><I> in place of <I>t.state<I> and <I>t.next.state<I>, representing the state for tick <I>t<I> and the state for its successor <I>t.next<I>. Note that this formulation precludes stuttering; we could admit it simply by adding the disjunct <I>s<I>=<I>s<\#48><I> allowing a transition that corresponds to no operation occurring.\r
+@body:Bear in mind that this fact is a constraint on all atoms in the set <I>SystemTrace<I>. As a free standing fact, the second line of the fact<\#151>the initial condition<\#151> would have been written:\r
+@geekmath:fact {all x: SystemTrace | Init ((x.first).(x.state))}\r
+@subsection:4.7 Abstraction\r
+@noindent:Abstraction relationships are easily expressed using our function syntax. To show that our memory system refines a simple memory without a cache, we define an abstraction function <I>Alpha<I> saying that a system corresponds to a memory that is like the system<\#48>s memory, overwritten by the entries of the system<\#48>s cache:\r
+@geekmath:fun Alpha (s: System, m: Memory) {<\n> m.map = s.main.map ++ s.cache.map<\n> } As another example, if our linked list were to represent a set, we might define the set corresponding to a given list as that containing the elements reachable from the start:\r
+@geekmath:fun ListAlpha (p: List, s: set Elt) {<\n> s = p.*rest.elt<\n> }\r
+@subsection:4.8 Assertions\r
+@noindent:Theorems about a specification are packaged as <I>assertions<I>. An assertion is simply a formula that is intended to hold. A tool can check an assertion by searching for a counterexample<\#151>that is, a model of the formula<\#48>s negation.\r
+@body:The simplest kinds of assertion record consequences of state properties. For example,\r
+@geekmath:assert {<\n> all s: System | DirtyInv (s) && no s.cache.dirty<\n> = s.cache.map in s.main.map<\n> }\r
+@noindent:asserts that if the dirtiness invariant holds,and there are no dirty addresses, then the mapping of addresses to data in the cache is a subset of the mapping in the main memory.\r
+@body:An assertion can express consequences of operations. For example,\r
+@geekmath:assert {<\n> all s: System, d: Data, a: Addr |<\n> SystemRead (s,d,a) = a in s.cache.addrs<\n> }\r
+@noindent:embodies the claim made above that <I>SystemRead<I> has an implicit precondition; it asserts that whenever <I>SystemRead<I> occurs for an address, that address must be in the cache beforehand. An assertion can likewise identify a consequence in the post<\#45>state; this assertion\r
+@geekmath:assert {<\n> all s,s<\#48>: System, d: Data, a: Addr |<\n> SystemWrite (s,s<\#48>,d,a) = s<\#48>.cache.map[a] = d<\n> } says that after a <I>SystemWrite<I>, the data value appears in the cache at the given address. Preservation of an invariant by an operation is easily recorded as an assertion. To check that our dirtiness invariant is preserved when writes occur, we would assert\r
+@geekmath:assert {<\n> all s,s<\#48>: System, d: Data, a: Addr |<\n> SystemWrite (s,s<\#48>,d,a) && DirtyInv (s) = DirtyInv (s<\#48>)<\n> }\r
+@noindent:Invariant preservation is not the only consequence of an operation that we would like to check that relates pre<\#45> and post<\#45>states. We might, for example, want to check that operations on the memory system do not change the set of addresses of the main memory. For the <I>Flush<I> operation, for example, the assertion would be\r
+@geekmath:assert {<\n> all s,s<\#48>: System | Flush(s,s<\#48>) = s.main.addrs = s<\#48>.main.addrs<\n> } which holds only because the cache addresses are guaranteed to be a subset of the main memory addresses (by the fact associated with the <I>System<I> signature).\r
+@noindent:The effect of a sequence of operations can be expressed by quantifying appropriately over states. For example, assert {<\n> all s, s<\#48>: System, a: Addr, d,d<\#48>: Data | <\n> SystemWrite (s,s<\#48>,d,a) && SystemRead (s<\#48>,d<\#48>,a) = d = d<\#48><\n> }\r
+@noindent:says that when a write is followed by a read of the same address, the read returns the data value just written.\r
+@body:To check that a property holds for all reachable states, we can assert that the property is an invariant of every operation, and is established by the initial condition. This strategy can be shown (by induction) to be sound, but it is not complete. A property may hold for all reachable states, but may not be preserved because an operation breaks the property when executed in a state that happens not to be reachable.\r
+@body:Traces overcome this incompleteness. Suppose, for example, that we want to check the (rather contrived) property that, in every reachable state, if the cache contains an address that isn<\#48>t dirty, then it agrees with the main memory on at least one address:\r
+@geekmath:fun DirtyProp (s: System) {<\n> some (s.cache.addrs <\#45> s.cache.dirty)<\n> = some a: Addr | s.cache.map[a] = s.main.map[a]<\n> }\r
+@noindent:We can assert that this property holds in the last state of every trace:\r
+@geekmath:assert {<\n> all t: SystemTrace | with t | DirtyProp (last.state)<\n> } This assertion is valid, even though <I>DirtyProp<I> is not an invariant. A write invoked in a state in which all clean entries but one had non<\#45>matching values can result in a state in which there are still clean entries but none has a matching value.\r
+@noindent:Finally, refinements are checked by assertions involving abstraction relations. We can assert that a <I>SystemWrite<I> refines a basic <I>Write<I> operation on a simple memory:\r
+@geekmath:assert {<\n> all s,s<\#48>: System, m,m<\#48>: Memory, a: Addr, d: Data |<\n> Alpha (s,m) && Alpha (s<\#48>,m<\#48>) && SystemWrite (s,s<\#48>,a,d)<\n> = Write (m,m<\#48>,a,d)<\n> }\r
+@noindent:or that the <I>Flush<I> operation is a no<\#45>op when viewed abstractly:\r
+@geekmath:assert {<\n> all s,s<\#48>: System, m,m<\#48>: Memory |<\n> Alpha (s,m) && Alpha (s<\#48>,m<\#48>) && Flush (s,s<\#48>)<\n> = m.map = m<\#48>.map<\n> }\r
+@noindent:Note the form of the equality; <I>m = m<\#48><I> would be wrong, since two distinct memories may have the same mapping, and the abstraction <I>Alpha<I> constrains only the mapping and not the memory atom itself.\r
+@body:Many of the assertions shown here can be made more succinct by the function shorthand explained in Section 3.7 below. For example, the assertion that a read following a write returns the value just written becomes:\r
+@geekmath:assert {<\n> all s: System, a: Addr, d: Data | <\n> SystemRead (SystemWrite (s,d,a),a) = d<\n> }\r
+@noindent:and the assertion that <I>Flush<I> is a no<\#45>op becomes:\r
+@geekmath:assert {<\n> all s: System | Alpha (s).map = Alpha (Flush (s)).map<\n> }\r
+@subsection:4.9 Polymorphism\r
+@noindent:Signatures can be parameterized by signature types. Rather than declaring a linked list whose elements belong to a particular type <I>Elt<I>, as above, we would prefer to declare a generic list:\r
+@geekmath:sig List [T] {}<\n> sig NonEmptyList [T] extends List [T] {elt: T, rest: List [T]}\r
+@noindent:Functions and facts may be parameterized in the same way, so we can define generic operators, such as:\r
+@geekmath:fun first [T] (p: List [T]): T {result = p.elt}<\n> fun last [T] (p: List [T]): T {some q: p.*rest | result = q.elt && no q.rest}<\n> fun elements [T] (p: List [T]): set T {result = p.*rest.elt}\r
+@noindent:In addition, let<\#48>s define a generic function that determines whether two elements follow one another in a list:\r
+@geekmath:fun follows [T] (p: List[T], a,b: T) {<\n> some x: p.*rest | x.elt = a && x.next.elt = b<\n> }\r
+@noindent:To see how a generic signature and operators are used, consider replacing the traces of Section 2.6 with lists of system states. Define a function that determines whether a list is a trace:\r
+@geekmath:fun isTrace (t: List [System]) {<\n> Init (first(t))<\n> all s, s<\#48>: System | follows (t,s,s<\#48>) = {<\n> Flush (s,s<\#48>)<\n> || (some a: Addr | Load (s,s<\#48>,a))<\n> || (some d: Data, a: Addr | SystemWrite (s,s<\#48>,d,a))<\n> }<\n> }\r
+@noindent:Now our assertion that every reachable system state satisfies <I>DirtyProp<I> can now be written:\r
+@geekmath:assert {<\n> all t: List[System] | isTrace(t) = DirtyProp (last(t))<\n> }\r
+@subsection:4.10 Variants\r
+@noindent:To illustrate the flexibility of our notation, we sketch a different formulation of state machines oriented around transitions rather than states.\r
+@body:Let<\#48>s introduce a signature representing state transitions of our memory system:\r
+@geekmath:sig SystemTrans {pre,post: System}<\n> {pre.main.addrs = post.main.addrs}\r
+@noindent:Declaring the transitions as a signature gives us the opportunity to record properties of all transitions<\#151>in this case requiring that the set of addresses of the main memory is fixed.\r
+@body:Now we introduce a subsignature for the transitions of each operation. For example, the transitions that correspond to load actions are given by:\r
+@geekmath:sig LoadTrans extends SystemTrans {a: Addr}<\n> {Load (pre, post, a)} \r
+@noindent:For each invariant, we define a set of states. For the states satisfying the dirty invariant, we might declare\r
+@geekmath:sig DirtyInvStates extends System {}\r
+@noindent:along with the fact\r
+@geekmath:fact {DirtyInvStates = {s: System | DirtyInv(s)}}\r
+@noindent:To express invariant preservation, it will be handy to declare a function that gives the image of a set of states under a set of transitions:\r
+@geekmath:fun postimage (ss: set System, tt: set SystemTrans): set System {<\n> result = {s: System | some t: tt | t.pre in ss && s = t.post}<\n> }\r
+@noindent:so that we can write the assertion like this:\r
+@geekmath:assert {postimage (DirtyInvStates, LoadTrans) in DirtyInvStates}\r
+@noindent:For an even more direct formulation of state machine properties, wemight have defined a transition relation instead:\r
+@geekmath:fun Trans (r: System <\#45> System) {<\n> all s, s<\#48> : System | <\n> s<\#45>s<\#48> in r = Flush (s,s<\#48>) || <\#133><\n> }\r
+@noindent:Then, using transitive closure, we can express the set of states reachable from an initial state, and assert that this set belongs to the set characterized by some property:\r
+@geekmath:assert {all r: System <\#45> System, s: System |<\n> Init (s) && Trans(r) = s.*r in DirtyPropStates<\n> }\r
+@noindent:where <I>DirtyPropStates<I> is defined analogously to <I>DirtyInvStates<I>.\r
+@subsection:4.11 Definitions\r
+@noindent:Instead of declaring the addresses of a memory along with its mapping, as we did before:\r
+@geekmath:sig Memory {<\n> addrs: set Addr,<\n> map: addrs <\#45>! Data<\n> }\r
+@noindent:we could instead have declared the mapping alone:\r
+@geekmath:sig Memory {<\n> map: Addr <\#45>? Data<\n> }\r
+@noindent:and then <I>defined<I> the addresses using a subsignature:\r
+@geekmath:sig MemoryWithAddrs extends Memory {<\n> addrs: set Addr}<\n> {addrs = {a: Addr | some a.map}} Now by making the subsignature subsume all memories:\r
+@geekmath:fact {Memory in MemoryWithAddrs}\r
+@noindent:we have essentially <\#145>retrofitted<\#146> the field. Any formula involving memory atoms now implicitly constrains the <I>addrs<I> field. For example, we can assert that <I>Read<I> has an implicit precondition requiring that the argument be a valid address:\r
+@geekmath:assert {all m: Memory, a: Addr, d: Data | Read (m,d,a) = a in m.addrs}\r
+@noindent:even though the specification of <I>Read<I> was written when the field <I>addrs<I> did not even exist.\r
+@section:5 Semantics\r
+@noindent:For completeness, we give an overview of the semantics of the language. The novelties with respect to the original version of Alloy [4] are (1) the idea of organizing relations around basic types as signatures, (2) the treatment of extension as subsetting, and (3) the packaging of formulas in a more explicit (and conventional) style. The semantic basis has been made cleaner, by generalizing relations to arbitrary arity, eliminating <\#145>indexed relations<\#146> and the need for a special treatment of sets.\r
+@subsection:5.1 Types\r
+@noindent:We assume a universe of atoms. The standard notion of a mathematical relation gives us our only composite datatype. The value of an expression will always be a relation<\#151>that is, a collection of tuples of atoms. Relations are first order: the elements of a tuple are themselves atoms and never relations.\r
+@body:The language is strongly typed. We partition the universe into subsets each associated with a <I>basic<I> type, and write (T<I>1, T<I>2, <\#133>, T<I>n) for the type of a relation whose tuples each consist of <I>n<I> atoms, with types T<I>1, T<I>2, etc.\r
+@body:A set is represented semantically as a unary relation, namely a relation whose tuples each contain one atom. A tuple is represented as a singleton relation, namely a relation containing exactly one tuple. A scalar is represented as a unary, singleton relation. We use the terms <\#145>set<\#146>, <\#145>tuple<\#146> and <\#145>scalar<\#146> to describe relations with the appropriate properties. Basic types are used only to construct relation types, and every expression that appears in a specification has a relational type. Often we will say informally that an expression has a type <I>T<I> where <I>T<I> is the name of a basic type when more precisely we mean that the expression has the type (<I>T<I>).\r
+@body:So, in contrast to traditional mathematical style, we do not make distinctions amongst the atom <I>a<I>, the tuple (<I>a<I>), the set {<I>a<I>} containing just the atom, or the set {(<I>a<I>)} containing the tuple, and represent all of these as the last. This simplifies the semantics and gives a more succinct and uniform syntax. \r
+@subsection:5.2 Expression Operators\r
+@noindent:Expressions can be formed using the standard set operators written as ASCII characters: union (+), intersection (&) and difference (<\#45>). Some standard relational operators, such as transpose (~) and transitive closure (^), can be applied to expressions that denote binary relations. Relational override (++) has its standard meaning for binary relations but can applied more broadly. \r
+@body:There are two special relational operators, dot and arrow. The dot operator is a generalized relational composition. Given expressions <I>p<I> and <I>q<I>, the expression <I>p<I>.<I>q<I> contains the tuple <f"Symbol"><\#225><f$><I>p<I><->1<->, <\#133> <I>p<I><-><I>m<I><\#45>1<->, <I>q<I><->2<->, <\#133>, <I>q<I><-><I>n<I><-><f"Symbol"><\#241><f$> when <I>p<I> contains @math @sep p<I>1, <\#133>, p<I>{m}, <I>q<I> contains @math @sep q<I>1, <\#133> q<I>n, and @math p<I>m = q<I>1. The last type of <I>p<I> and the first type of <I>q<I> must match, and <I>m<I> + <I>n<I>, the sum of the arities of <I>p<I> and <I>q<I>, must be three or more so that the result is not degenerate. When <I>p<I> is a set and <I>q<I> is a binary relation, the composition <I>p.q<I> is the standard relational image of <I>p<I> under <I>q<I>; when <I>p<I> and <I>q<I> are both binary relations, <I>p.q<I> is standard relational composition. In all of the examples above, the dot operator is used only for relational image.\r
+@body:The arrow operator is cross product: <I>p q<I> is the relation containing the tuple @math @sep p<I>1, <\#133>, p<I>{m}, q<I>1, <\#133> q<I>n when <I>p<I> contains @math @sep p<I>1, <\#133>, p<I>{m}, and <I>q<I> contains @math @sep q<I>1, <\#133> q<I>n. In all the examples in this paper, <I>p<I> and <I>q<I> are sets, and <I>p q<I> is their standard cross product.\r
+@subsection:5.3 Formula Operators\r
+@noindent:Elementary formulas are formed from the subset operator, written <I>in<I>. Thus <I>p in q<I> is true when every tuple in <I>p<I> is in <I>q<I>. The formula <I>p : q<I> has the same meaning, but when <I>q<I> is a set, adds an implicit constraint that <I>p<I> be scalar (ie, a singleton). This constraint is overridden by writing <I>p: option q<I> (which lets <I>p<I> to be empty or a scalar) or <I>p: set q<I> (which eliminates the constraint entirely). Equality is just standard set equality, and is short for a subset constraint in each direction.\r
+@body:An arrow that appears as the outermost expression operator on the right<\#45>hand side of a subset formula can be annotated with <I>multiplicity markings<I>: + (one or more), ? (zero or one) and ! (exactly one). The formula\r
+@geekmath:r: S m n T\r
+@noindent:where <I>m<I> and <I>n<I> are multiplicity markings constrains the relation <I>r<I> to map each atom of <I>S<I> to <I>n<I> atoms of <I>T<I>, and to map <I>m<I> atoms of <I>S<I> to each atom of <I>T<I>. <I>S<I> and <I>T<I> may themselves be product expressions, but are usually variables denoting sets. For example,\r
+@geekmath:r: S ! T<\n> r: S ? ! T\r
+@noindent:make <I>r<I> respectively a total function on <I>S<I> and an injection.\r
+@body:Larger formulas are obtained using the standard logical connectives: && (and), || (or), ! (not), =<I> (implies), iff<I> (bi<\#45>implication). The formula <I>if b then f else g<I> is short for <I>b<I> =<I> f<I> && !<I>b<I> =<I> g<I>. Within curly braces, consecutive formulas are implicitly conjoined.\r
+@body:Quantifications take their usual form:\r
+@geekmath:all x: e | F\r
+@noindent:is true when the formula <I>F<I> holds under every binding of the variable <I>x<I> to a member of the set <I>e<I>. In addition to the standard quantifiers, <I>all<I> (universal) and <I>some<I> (existential), we have <I>no<I>, <I>sole<I> and <I>one<I> meaning respectively that there are no values, at most one value, and exactly one value satisfying the formula. For a quantifier <I>Q<I> and expression <I>e<I>, the formula <I>Q e<I> is short for <I>Q x: T | e<I> (where <I>T<I> is the type of <I>e<I>), so <I>no e<I>, for example, says that <I>e<I> is empty.\r
+@body:The declaration of a quantified formula is itself a formula<\#151>an elementary formula in which the left<\#45>hand side is a variable. Thus\r
+@geekmath:some x = e | F\r
+@noindent:is permitted, and is a useful way to express a <I>let<I> binding. Quantifiers may be higher<\#45>order; the formula\r
+@geekmath:all f: s <\#45><I>! t | F\r
+@noindent:is true when F<I> holds for every binding of a total function from <I>s<I> to <I>t<I> to the variable <I>f<I>. Our analysis tool cannot currently handle higher<\#45>order quantifiers, but many uses of higher<\#45>order quantifiers that arise in practice can be eliminated by skolemization.\r
+@body:Finally, we have relational comprehensions; the expression\r
+@geekmath:{x<I>1: e<I>1, x<I>2: e<I>2, <\#133> | F}\r
+@noindent:constructs a relation of tuples with elements <I>x<I>1<I>, <I>x<I>2<I>, etc., drawn from set expressions <I>e<I>1<I>, <I>e<I>2<I>, etc., whose values satisfy <I>F<I>.\r
+@body:Signatures\r
+@noindent:A <I>signature<I> declaration introduces a basic type, along with a collection of relations called <I>fields<I>. The declaration\r
+@geekmath:sig S {f: E}\r
+@noindent:declares a basic type <I>S<I>, and a relation <I>f<I>. If <I>E<I> has the type (T<I>1, T<I>2, <\#133>, T<I>n), the relation <I>f<I> will have the type (S, T<I>1, T<I>2, <\#133>, T<I>n), and if <I>x<I> has the type <I>S<I>, the expression <I>x.f<I> will have the same type as <I>E<I>. When there are several fields, field names already declared may appear in expressions on the right<\#45>hand side of declarations; in this case, a field <I>f<I> is typed as if it were the expression <I>this.f<I>, where <I>this<I> denotes an atom of the signature type (see Section 3.6).\r
+@body:The meaning of a specification consisting of a collection of signature declarations is an assignment of values to global constants<\#150> the signatures and the fields. For example, the specification\r
+@geekmath:sig Addr {}<\n> sig Data {}<\n> sig Memory {map: Addr <\#45><I> Data}\r
+@noindent:has 4 constants<\#151>the three signatures and one field<\#151>with assignments such as:\r
+@geekmath:Addr = {a0, a1}<\n> Data = {d0, d1, d2}<\n> Memory = {m0, m1}<\n> map = {(m0,a0,d0), (m1,a0,d1), (m1,a0,d2)}\r
+@noindent:corresponding to a world in which there are 2 addresses, 3 data values and 2 memories, with the first memory (m0<I>) mapping the first address (<I>a0<I>) to the first data value (<I>d0<I>), and the second memory (<I>m1<I>) mapping the first address (<I>a0<I>) both to the second (<I>d1<I>) and third (<I>d2<I>) data values.\r
+@body:A fact is a formula that constrains the constants of the specification, and therefore tends to reduce the set of assignments denoted by the specification. For example,\r
+@geekmath:fact {all m: Memory | all a: Addr | sole m.map[a]}\r
+@noindent:rules out the above assignment, since it does not permit a memory (such as <I>m1<I>) to map an address (such as <I>a0<I>) to more than one data value. The meaning of a function is a set of assignments, like the meaning of the specification as a whole, but these include bindings to parameters. For example, the function\r
+@geekmath:fun Read (m: Memory, d: Data, a: Addr) {<\n> d = m.map[a]<\n> }\r
+@noindent:has assignments such as:\r
+@geekmath:Addr = {a0, a1}<\n> Data = {d0, d1, d2}<\n> Memory = {m0, m1}<\n> map = {(m0,a0,d1)}<\n> m = {m0}<\n> d = {d1}<\n> a = {a0}\r
+@noindent:The assignments of a function representing a state invariant correspond to states satisfying the invariant; the functions of a function representing an operation (such as <I>Read<I>) correspond to executions of the operation.\r
+@body:An assertion is a formula that is claimed to be <I>valid<I>: that is, true for every assignment that satisfies the facts of the specification. To check an assertion, one can search for a <I>counterexample<I>: an assignment that makes the formula false. For example, the assertion\r
+@geekmath:assert {<\n> all m,m<\#48>: Memory, d: Data, a: Addr | Read (m,d,a) =<I> Read (m<\#48>,d,a)}\r
+@noindent:which claims, implausibly, that if a read of memory m<I> returns <I>d<I> at <I>a<I>, then so does a read at memory <I>m<\#48><I>, has the counterexample\r
+@geekmath:Addr = {a0}<\n> Data = {d0,d1}<\n> Memory = {m0, m1}<\n> map = {(m0,a0,d0), (m1,a0,d1)}\r
+@noindent:To find a counterexample, a tool should negate the formula and then skolemize away the bound variables, treating them like the parameters of a function, with values to be determined as part of the assignment. In this case, the assignment might include:\r
+@geekmath:m = {m0}<\n> m<\#48> = {m1}<\n> d = {d0}<\n> a = {a0}\r
+@subsection:5.4 Extension\r
+@noindent:Not every signature declaration introduces a new basic type. A signature declared without an extension clause is a <I>type signature<I>, and creates both a basic type and a set constant of the same name. A signature <I>S<I> declared as an extension is a <I>subsignature<I>, and creates only a set constant, along with a constraint making it a subset of each <I>supersignature<I> listed in the extension clause. The subsignature takes on the type of the supersignatures, so if there is more than one, they must therefore have the same type, by being direct or indirect subsignatures of the same type signature.\r
+@body:A field declared in a subsignature is as if declared in the corresponding type signature, with the constraint that the domain of the field is the subsignature. For example,\r
+@geekmath:sig List {}<\n> sig NonEmptyList extends List {elt: Elt,rest: List}\r
+@noindent:makes <I>List<I> a type signature, and <I>NonEmptyList<I> a subset of <I>List<I>. The fields <I>elt<I> and <I>rest<I> map atoms from the type <I>List<I>, but are constrained to have domain <I>NonEmptyList<I>. Semantically, it would have been equivalent to declare them as fields of <I>List<I>, along with facts constraining their domains:\r
+@geekmath:sig List {elt: Elt,rest: List}<\n> sig NonEmptyList extends List {}<\n> fact {elt.Elt in NonEmptyList}<\n> fact {rest.List in NonEmptyList}\r
+@noindent:(exploiting our dot notation to write the domain of a relation <I>r<I> from <I>S<I> to <I>T<I> as <I>r.T<I>).\r
+@subsection:5.5 Overloading and Implicit Prefixing\r
+@noindent:Whenever a variable is declared, its type can be easily obtained from its declaration (from the type of the expression on the right<\#45>hand side of the declaration), and every variable appearing in an expression is declared in an enclosing scope. The one complication to this rule is the typing of fields.\r
+@body:For modularity, a signature creates a local namespace. Two fields with the name <I>f<I> appearing in different signatures do not denote the same relational constant. Interpreting an expression therefore depends on first resolving any field names that appear in it. #We have devised a simple resolution scheme whose details are beyond the scope of this paper. In an expression of the form <I>e.f<I>, the signature to which <I>f<I> belongs is determined according to the type of <I>e<I>. To keep the scheme simple, we require that sometimes the specifier resolve the overloading explicitly by writing the field <I>f<I> of signature <I>S<I> as <I>S<I>f<I><I>. (<I>At<I> <I>the<I> <I>end<I> <I>of<I> <I>the<I> <I>previous<I> <I>section<I>, <I>for<I> <I>example<I>, <I>the<I> <I>reference<I> <I>in<I> <I>the<I> <I>fact<I> <I>to<I> <I><I>rest<I><I> <I>should<I> <I>actually<I> <I>be<I> <I>to<I> <I><I>List<I>rest<I>, since the context does not indicate which signature <I>rest<I> belongs to.)\r
+@body:In many formulas, a single expression is dereferenced several times with different fields. A couple of language features are designed to allow these formulas to be written more succinctly, and, if used with care, more comprehensibly. First, we provide two syntactic variants of the dot operator. Both <I>p<I>::<I>q<I> and <I>q<I>[<I>p<I>] are equivalent to <I>p.q<I>, but have different precedence: the double colon binds more tightly than the dot, and the square brackets bind more loosely than the dot. Second, we provide a <I>with<I> construct similar to Pascal<\#48>s that makes dereferencing implicit.\r
+@body:Consider, for example, the following simplified signature for a trace:\r
+@geekmath:sig Trace {<\n> ticks: set Tick,<\n> first: Tick,<\n> next: Tick <\#45><I> Tick,<\n> state: Tick <\#45> State<\n> }\r
+@noindent:Each trace t<I> has a set of ticks <I>t.ticks<I>, a first tick <I>t.first<I>, an ordering <I>t.next<I> that maps ticks to ticks, and a relation <I>t.state<I> mapping each tick to a state. For a trace <I>t<I> and tick <I>k<I>, the state is <I>k<I>.(<I>t.state<I>); the square brackets allow this expression to be written instead as <I>t.state<I>[<I>k<I>]. To constrain <I>t.ticks<I> to be those reachable from <I>t. first<I> we might write:\r
+@geekmath:fact {all t: Trace | (t.first).*(t.next ) = t.ticks}\r
+@noindent:Relying on the tighter binding of the double colon, we can eliminate the parentheses:\r
+@geekmath:fact {all t: Trace | t::first.*t::next = t.ticks}\r
+@noindent:Using <I>with<I>, we can make the <I>t<I> prefixes implicit:\r
+@geekmath:fact {all t: Trace | with t | first.*next = ticks}\r
+@noindent:In general, <I>with e | F<I> is like <I>F<I>, but with <I>e<I> prefixed wherever appropriate to a field name. Appropriateness is determined by type: <I>e<I> is matched to any field name with which it can be composed using the dot operator. A fact attached to a signature <I>S<I> is implicitly enclosed by <I>all this: S | with this |<I>, and the declarations of a signature are interpreted as constraints as if they had been declared within this scope. Consequently, the declaration of <I>first<I> above should be interpreted as if it were the formula:\r
+@geekmath:all this: Trace | with this | first: ticks\r
+@noindent:which is equivalent to\r
+@geekmath:all this: Trace | this.first: this.ticks\r
+@noindent:and should be typed accordingly. \r
+@subsection:5.6 Function Applications\r
+@noindent:A function may be applied by binding its parameters to expressions. The resulting application may be either an expression or a formula, but in both cases the function body is treated as a formula. The formula case is simple: the application is simply short for the body with the formal parameters replaced by the actual expressions (and bound variables renamed where necessary to avoid clashes).\r
+@body:The expression case is more interesting. The application is treated as a syntactic sugar. Suppose we have a function application expression, <I>e<I> say, of the form\r
+@geekmath:f(a<I>1, a<I>2, <\#133>, a<I>n)\r
+@noindent:that appears in an elementary formula <I>F<I>. The declaration of the function <I>f<I> must list <I>n<I> + 1 formal arguments, of which the <I>second<I> will be treated as the result. The entire elementary formula is taken to be short for\r
+@geekmath:all result: D | f (a<I>1, result, a<I>2, <\#133>, a<I>n) =<I> F [result/e]\r
+@noindent:where D<I> is the right<\#45>hand side of the declaration of the missing argument, and <I>F<I> [<I>result<I>/<I>e<I>] is <I>F<I> with the fresh variable <I>result<I> substituted for the application expression <I>e<I>. The application of <I>f<I> in this elaborated formula is now a formula, and is treated simply as an inlining of the formula of <I>f<I>.\r
+@body:To see how this works, consider the definition of a function <I>dom<I> that gives the domain of a relation over signature <I>X<I>:\r
+@geekmath:fun dom (r: X <\#45><I> X, d: set X) {d = r.X}\r
+@noindent:(We have defined the function monomorphically for a homogeneous relation. In practice, one would define a polymorphic function, but we want to avoid conflating two unrelated issues.) Here is a trivial assertion that applies the function as an expression:\r
+@geekmath:assert {all p: X X | (dom (p)).p in X}\r
+@noindent:Desugaring the formula, we get\r
+@geekmath:all p: X X | all result: set X | dom (p, result) = result.p in X\r
+@noindent:and then inlining\r
+@geekmath:all p: X X | all result: set X | result = p.X = result.p in X\r
+@noindent:This formula can be reduced (by applying a universal form of the One Point Rule) to\r
+@geekmath:all p: X X | (p.X).p in X\r
+@noindent:which is exactly what would have been obtained had we just replaced the application expression by the expression on the right<\#45>hand side of the equality in the function<\#48>s definition! \r
+@body:Now let<\#48>s consider an implicit definition. Suppose we have a signature X<I> with an ordering <I>lte<I>, so that <I>e.lte<I> is the set of elements that <I>e<I> is less than or equal to, and a function <I>min<I> that gives the minimum of a set, defined implicitly as the element that is a member of the set, and less than or equal to all members of the set:\r
+@geekmath:sig X {lte: set X}<\n> fun min (s: set X, m: option X) {<\n> m in s && s in m.lte<\n> }\r
+@noindent:Because the set may be empty, <I>min<I> is partial. Depending on the properties of <I>lte<I> it may also fail to be deterministic. A formula that applies this function\r
+@geekmath:assert {all s: set X | min (s) in s}\r
+@noindent:can as before be desugared\r
+@geekmath:all s: set X | all result: option X | min (s, result) =<I> result in s\r
+@noindent:and expanded by inlining\r
+@geekmath:all s: set X | all result: option X |<\n> (result in s) && s in result.lte = result in s\r
+@noindent:but in this case the One Point Rule is not applicable.\r
+@body:As a convenience, our language allows the result argument of a function to be declared anonymously in a special position, and given the name result<I>. The domain function, for example, can be defined as:\r
+@geekmath:fun dom (r: X <\#45><I> X): set X {result = r.X}\r
+@noindent:How the function is defined has no bearing on how it is used; this definition is entirely equivalent to the one above, and can also be applied as a formula with two arguments.\r
+@subsection:5.7 Polymorphism\r
+@noindent:Polymorphism is treated as a syntactic shorthand. Lack of space does not permit a full discussion here.\r
+@section:6 Related Work\r
+@noindent:We have shown how a handful of elements can be assembled into a rather simple but flexible notation. The elements themselves are far from novel<\#151>indeed, we hope that their familiarity will make the notation easy to learn and use<\#151>but their assembly into a coherent whole results in a language rather different from existing specification languages.\r
+@subsection:6.1 New Aspects\r
+@noindent:The more novel aspects of our work are:\r
+@point:\alpha 6.1.A Objectification of state<I>. Most specification languages represent states as cartesian products of components; in our approach, a state, like a member of any signature, is an individual<\#151>a distinct atom with identity. A similar idea is used in the situation calculus [11], whose <\#145>relational fluents<\#146> add a situation variable to each time<\#45>varying relation. The general idea of objectifying all values is of course the foundation of object<\#45>oriented programming languages, and was present in LISP. Interestingly, object<\#45>oriented variants of Z (such as [1]) do not objectify schemas. The idea of representing structures in first<\#45>order style as atoms is present also in algebraic specifications such as Larch [2], which treat even sets and relations in this manner.\r
+@point:\alpha 6.1.B <I>Components as relations<I>. Interpreting fields of a structure as functions goes back to early work on verification, and is widely used (for example, by Leino and Nelson [10]). We are not aware, however, of specification languages that use this idea, or that flatten fields to relations over atoms.\r
+@point:\alpha 6.1.C <I>Extension by global axioms<I>. The <\#145>facts<\#146> of our notation allow the properties of a signature to be extended monotonically. The idea of writing axioms that constrain the members of a set constant declared globally is hardly remarkable, but it appears not to have been widely exploited in specification languages.\r
+@point:\alpha 6.1.D <I>Extension by subset<I>. Treating the extension of a structure as a refinement modelled by subset results in a simple semantics, and melds well with the use of global axioms. Again, this seems to be an unremarkable idea, but one whose power has not been fully recognized.\r
+@subsection:6.2 Old Aspects\r
+@noindent:The aspects of our work that are directly taken from existing languages are:\r
+@point:\alpha 6.2.A <I>Formulas<I>. The idea of treating invariants, definitions, operations, etc, uniformly as logical formulas is due to Z [14].\r
+@point:\alpha 6.2.B <I>Assertions<I>. Larch [2] provides a variety of constructs for adding intentional redundancy to a specification in order to provide error<\#45>detection opportunities. <I>Parameterized formulas<I>. The <\#145>functional<\#146> style we have adopted, in which all formulas are explicitly parameterized, in contrast to the style of most specification languages, is used also by languages for theorem provers, such as PVS [13]. VDM [8] offers a mechanism called <\#145>operation quotation<\#146> in which pre<\#45> and post conditions are reused by interpreting them as functions similar to ours.\r
+@point:\alpha 6.2.C <I>Parametric Polymorphism<I>. The idea of parameterizing descriptions by types was developed in the programming languages community, most notably in the context of ML [12].\r
+@point:\alpha 6.2.D <I>Implicit Prefixing<I>. Our <\#145>with<\#146> operator is taken from Pascal [9].\r
+@point:\alpha 6.2.E <I>Relational operators<I>. The dot operator, and the treament of scalars as singletons, comes from the earlier version of Alloy [4]. \r
+@subsection:6.3 Z<\#48>s Schema Calculus\r
+@noindent:Z has been a strong influence on our work; indeed, this paper may be viewed as an attempt to achieve some of the power and flexibility of Z<\#48>s schema calculus in a first<\#45>order setting. Readers unfamiliar with Z can find an excellent presentation of the schema calculus in [16]. The current definitive reference is [15], although Spivey<\#48>s manual [14] is more accessible for practioners.\r
+@body:A <I>schema<I> consists of a collection of variable declarations and a formula constraining the variables. Schemas can be anonymous. When a name has been bound to a schema, it can be used in three different ways, distinguished according to context. First, it can be used as a <I>declaration<I>, in which case it introduces its variables into the local scope, constraining them with its formula. Second, where the variables are already in scope, it can be used as a <I>predicate<I>, in which case the formula applies and no new declarations are added. Both of these uses are syntactic; the schema can be viewed as a macro.\r
+@body:In the third use, the schema is semantic. Its name represents a set of <I>bindings<I>, each binding being a finite function from variables names to values. The bindings denoted by the schema name are the models of the schema<\#48>s formula: those bindings of variable names to values that make the formula true.\r
+@body:How a schema is being applied is not always obvious; in the set comprehension {<I>S<I>}, for example, <I>S<I> represents a declaration, so that the expression as a whole denotes the same set of bindings as <I>S<I> itself. Given a binding <I>b<I> for a schema with component variable <I>x<I>, the expression <I>b.x<I> denotes the value assigned to <I>x<I> in <I>b<I>. Unlike Alloy<\#48>s dot, this dot is a function application, so for a set of bindings <I>B<I>, the expression <I>B.x<I> is not well formed.\r
+@body:Operations in Z are expressed using the convention that primed variables denote components of the post<\#45>state. A mechanism known as <I>decoration<I> allows one to write <I>S<\#48><I> for the schema that is like <I>S<I>, but whose variable names have been primed. Many idioms, such as promotion, rely on being able to manipulate the values of a schema<\#48>s variables in aggregate. To support this, Z provides the theta operator: <f"Symbol"><\#113><f$> @sep <I>S<I> is an expression that denotes a binding in which each variable <I>x<I> that belongs to <I>S<I> is bound to a variable of the same name <I>x<I> declared in the local scope. Theta and decoration interact subtly: <f"Symbol"><\#113><f$> @sep <I>S<\#48><I> is not a binding of <I>S<\#48><I>, but rather binds each variable <I>x<I> of <I>S<I> to a variable <I>x<\#48><I> declared locally. So where we would write <I>s=s<\#48><I> to say that pre<\#45> and post<\#45>states <I>s<I> and <I>s<\#48><I> are the same, a Z specifier would write <f"Symbol"><\#113><f$> @sep <I>S<I> = <f"Symbol"><\#113><f$> @sep <I>S<\#48><I>. This formula equates each component <I>x<I> of <I>S<I> to its matching component <I>x<\#48><I> of <I>S<\#48><I>, because <I>x<I> and <I>x<\#48><I> are the respective values bound to <I>x<I> by <f"Symbol"><\#113><f$> @sep <I>S<I> and <f"Symbol"><\#113><f$> @sep <I>S<\#48><I> respectively.\r
+@body:Our <\#145>fact<\#146> construct allows the meaning of a signature name to be constrained subsequent to its declaration. A schema, in contrast, is <\#145>closed<\#146>: a new schema name must be introduced for each additional constraint. This can produce an undesirable proliferation of names for a system<\#48>s state, but it does make it easier to track down those formulas that affect a schema<\#48>s meaning.\r
+@body:The variables of a schema can be renamed, but cannot be replaced by arbitrary expressions (since this would make nonsense of declarations).This requires the introduction of existential quantifiers where in our notation an expression is passed as an actual. On the other hand, when no renaming is needed, it is more succinct.\r
+@body:Z<\#48>s sequential composition operator is defined by a rather complicated transformation, and relies on adherence to particular conventions. The schema <I>P<I> @sep @sep <I>Q<I> is obtained by collecting primed variables in <I>P<I> that match unprimed variables in <I>Q<I>; renaming these in both <I>P<I> and <I>Q<I> with a new set of variable names; and then existentially quantifying the new names away. For example, to say that a read following a write to the same address yields the value written, we would write:\r
+@geekmath:all m: Memory, a: Addr, d, d<\#48>: Data | Read (Write(m,a,d),d<\#48>) =<I> d = d<\#48>\r
+@noindent:which is short for\r
+@geekmath:all m: Memory, a: Addr, d, d<\#48>: Data |<\n> all m<\#48>: Memory | Write (m,m<\#48>,a,d) = Read (m,a,d<\#48>) = d = d<\#48>\r
+@noindent:In Z, assuming appropriate declarations of a schema Memory<I> and a given type <I>Data<I>, the formula would be:\r
+@geekmath: Memory; Memory<\#48>; x!: Data Write Read [x!/d!] x! = d!\r
+@noindent:which is short for\r
+@geekmath: Memory; Memory<\#48>; x!: Data <\n> Memory<\#48><\#145> <\n> Memory<\#146> Write <f"Symbol"><\#113><f$> @sep Memory<\#48> = <f"Symbol"><\#113><f$> @sep Memory<\#48><\#145><\n> Memory<\#146>; d!: Data <\n> Read <f"Symbol"><\#113><f$> @sep Memory = <f"Symbol"><\#113><f$> @sep Memory<\#48><\#145> d! = x!<\n> x! = d!\r
+@noindent:The key semantic difference between signatures and schemas is this. A signature is a set of atoms; its fields are relational constants declared in global scope. A schema, on the other hand, denotes a higher<\#45>order object: a set of functions from field names to values. Our approach was motivated by the desire to remain first order, so that the analysis we have developed [3] can be applied. Not surprisingly, there is a cost in expressiveness. We cannot express higher<\#45>order formulas, most notably those involving preconditions. Suppose we want to assert that our write operation has no implicit precondition. In Z, such an assertion is easily written:\r
+@geekmath: Memory; a?: Addr Memory<\#48>; d!: Data Write\r
+@noindent:We might attempt to formulate such an assertion in our notation as follows:\r
+@geekmath:assert {<\n> all m: Memory, a: Addr, d: Data | some m<\#48>: Memory | Write (m,m<\#48>,d,a) }\r
+@noindent:Unfortunately, this has counterexamples such as\r
+@geekmath:Addr = {a0}<\n> Data = {d0}<\n> Memory = {m0, m1}<\n> map = {}\r
+@noindent:in which the <I>map<I> relation lacks an appropriate tuple. Intuitively, the assertion claims that there is no context in which a write cannot proceed; a legitimate counterexample<\#151>but one we certainly did not intend<\#151>simply gives a context in which a memory with the appropriate address<\#45>value mapping is not available.\r
+@body:We have focused in this discussion on schemas. It is worth noting that Z is expressive enough to allow a style of structuring almost identical to ours, simply by declaring signatures as given types, fields and functions as global variables, and by writing facts, and the bodies of functions, as axioms. Field names would have to be globally unique, and the resulting specification would likely be less succinct than if expressed in our notation.\r
+@subsection:6.4 Phenomenology\r
+@noindent:Pamela Zave and Michael Jackson have developed an approach to composing descriptions [18] that objectifies states, events and time intervals, and constrains their properties with global axioms. Objectification allows descriptions to be reduced to a common phenomenology, so that descriptions in different languages, and even in different paradigms can be combined. Michael Jackson has argued separately for the importance of objectification as a means of making a more direct connection between a formal description and the informal world: as he puts it, <\#147>domain phenomena are facts about individuals<\#148> [7]. It is reassuring that the concerns of language design and tractability of analysis that motivated our notation are not in conflict with sound method, and it seems that our notation would be a good choice for expressing descriptions in the form that Zave and Jackson have proposed.\r
+@section:7 Evaluation\r
+@subsection:7.1 Merits\r
+@noindent:The key motivations of the design of our mechanism have been minimality and flexibility. It is worth noting how this has been achived by the <I>omission<I> of certain features:\r
+@point:\alpha 7.1.A There is only one form of semantic structuring; our opinion is that adding extra mechanisms, for example to group operations into classes, does not bring enough benefit to merit the additional complexity, and tends to be inflexible. (Our language does provide some namespace control for signature and paragraph names in the style of Java packages, but this is trivial and does not interact with the basic mechanism).\r
+@point:\alpha 7.1.B There is no subtyping; subsignatures are just subsets of their supersignatures, and have the same type. There are only two types: basic types (for signatures), and relational types (for expressions). Types are not nested.\r
+@point:\alpha 7.1.C There is only one way that formulas are packaged for reuse. The same function syntax is used for observers, operations, refinement relations, etc. The function shorthand syntax unifies the syntax of both declaration and use for explicit and implicit function definitions.\r
+@point:\alpha 7.1.D The values of a signature with fields are just like the values of any basic type; there is nothing like Z<\#48>s notion of a schema binding.\r
+@noindent:Our interpretation of a subsignature as a subset of the supersignature appears to be novel as a mechanism for structuring in a specification language. It has three nice consequences:\r
+@point:\alpha 7.1.E <I>Elimination of type coercions<I>. If <I>x<I> belongs to a signature <I>S<I> whose extension <I>S<\#48><I> defines a field <I>f<I>, the expression <I>x.f<I> will just denote an empty set if <I>x<I> does not belong to <I>S<\#48><I>. Contrast this with the treatment of subclasses in the Object Constraint Language [17], for example, which results in pervasive coercions and often prevents the use of set and relation operators (since elements must be coerced one at a time).\r
+@point:\alpha 7.1.F <I>Ease of extension<I>. Constraints can be added to the subsignature simply by writing a constraint that is universally quantified over elements of that subset.\r
+@point:\alpha 7.1.G <I>Definitional extension<I>. We can declare an extension <I>S<\#48><I> of a signature <I>S<I> with additional fields, relate these fields to the fields declared explicitly for <I>S<I>, and then record the fact that <I>S=S<\#48><I> (as illustrated in Section 2.11). The effect is that every atom of <I>S<I> has been extended with appropriately defined fields, which can be accessed whenever an expression denoting such an atom is in scope! We expect to find this idiom especially useful for defining additional fields for visualization purposes.\r
+@subsection:7.2 Deficiencies\r
+@noindent:One might wonder whether, having encoded structures using atoms, and having provided quantifiers over those atoms, one can express arbitrary properties of higher<\#45>order structures. Unfortunately, but not surprisingly, this is not possible. The catch is that fields are treated in any formulas as global variables that are existentially quantified. To simulate higher<\#45>order logic, it would be necessary to allow quantifications over these variables, and since they have relational type, that would imply higher<\#45>order quantification. The practical consequence is that properties requiring higher<\#45>order logic cannot be expressed. One cannot assert that the precondition of an operation is no stronger than some predicate; one cannot in general specify operations by minimization; and one cannot express certain forms of refinement check. An example of this problem is given in Section 4.3 above. Whether the problem is fundamental or can be partially overcome remains to be seen.\r
+@body:The treatment of subsignatures as subsets has a nasty consequence. Since a field declared in a subsignature becomes implicitly a field of the supersignature, two subsignatures cannot declare fields of the same name. The extension mechanism is therefore not properly modular, and a specification should use hierarchical structure instead where this matters.\r
+@body:Modelling a set of states as atoms entails a certain loss of abstraction. In this specification\r
+@geekmath:sig A {}<\n> sig S {a: A}<\n> fun op (s,s<\#48>: S) {s.a = s<\#48>.a}\r
+@noindent:the operation <I>op<I> has executions in which the pre<\#45> and post<\#45>states are equal (that is, the same atom in <I>S<I>), and executions in which only their <I>a<I> components are equal. One might object that this distinction is not observable. Moreover, replacing the formula by <I>s=s<\#48><I> would arguably be an overspecification<\#151>a <\#145>bias<\#146> in VDM terminology [8]. The situation calculus [11] solves this problem by requiring every operation to produce a state change: <I>s<I> and <I>s<\#48><I> are thus regarded as distinct situations by virtue of occurring at different points in the execution. The dual of this solution is to add an axiom requiring that no two distinct atoms of <I>S<I> may have equal <I>a<I> fields. Either of these solutions is easily imposed in our notation.\r
+@body:Our treatment of scalars and sets uniformly as relations has raised the concern that the resulting succinctness comes with a loss of clarity and redundancy. Extensive use of the previous version of our language, mostly by inexperienced specifiers, suggests that this is not a problem. The loss of some static checking is more than compensated by the semantic analysis that our tool performs.\r
+@section:8 Conclusion\r
+@noindent:Two simple ideas form the basis of our modularity mechanism: (1) that a structure is just a set of atoms, and its fields are global relations that map those atoms to structure components; and (2) that extensions of a structure are just subsets. Our relational semantics, in which all variables and fields are represented as relations, makes the use of structures simple and succinct, and it ensures that the language as a whole remains first order. For a variety of modelling tasks, we believe that our approach provides a useful balance of expressiveness and tractability.\r
+@section:9 Acknowledgments\r
+@noindent:The language described here was refined by experience writing specifications, long before an analyzer existed, and by the development of the analyzer tool itself. Mandana Vaziri and Sarfraz Khurshid were our early adopters, and Brian Lin and Joe Cohen helped implement the tool. The paper itself was improved greatly by comments from Mandana and Sarfraz, from Michael Jackson, from Tomi Mannisto, and especially from Pamela Zave, whose suggestions prompted a major rewrite. Jim Woodcock helped us understand Z, and the clarity and simplicity of his own work has been a source of inspiration to us. Our ideas have also been improved by the comments of the members of IFIP working groups 2.3 and 2.9, especially Tony Hoare, Greg Nelson and Rustan Leino. This work was funded in part by ITR grant #0086154 from the National Science Foundation, by a grant from NASA, and by an endowment from Doug and Pat Ross.\r
+@section:10 References\r
+@noindent:[1] R. Duke, G. Rose and G. Smith. Object<\#45>Z: A Specification Language Advocated for the Description of Standards. SVRC Technical Report 94<\#45>45. The Software Verification Research Centre, University of Queensland, Australia.\r
+@ref:[2] John V. Guttag, James J. Horning, and Andres Modet. Report on the Larch Shared Language: Version 2.3. Technical Report 58, Compaq Systems Research Center, Palo Alto, CA, 1990.\r
+@ref:[3] Daniel Jackson. Automating first<\#45>order relational logic. Proc. ACM SIGSOFT Conf. Foundations of Software Engineering. San Diego, November 2000.\r
+@ref:[4] Daniel Jackson. Alloy: A Lightweight Object Modelling Notation. To appear, ACM Transactions on Software Engineering and Methodology, October 2001.\r
+@ref:[5] Daniel Jackson, Ian Schechter and Ilya Shlyakhter. Alcoa: the Alloy Constraint Analyzer. Proc. International Conference on Software Engineering, Limerick, Ireland, June 2000.\r
+@ref:[6] Daniel Jackson and Jeannette Wing. Lightweight Formal Methods. In: H. Saiedian (ed.), An Invitation to Formal Methods. IEEE Computer, 29(4):16<\#45>30, April 1996. [7] Michael Jackson. Software Requirements and Specifications: A Lexicon of Practice, Principles and Prejudices. Addison<\#45>Wesley, 1995.\r
+@ref:[8] Cliff Jones. Systematic Software Development Using VDM. Second edition, Prentice Hall, 1990.\r
+@ref:[9] Kathleen Jensen and Nicklaus Wirth. Pascal: User Manual and Report. Springer<\#45># Verlag, 1974.\r
+@ref:[10] K. Rustan M. Leino and Greg Nelson. Data abstraction and information hiding . Research Report 160, Compaq Systems Research Center, November 2000.\r
+@ref:[11] Hector Levesque, Fiora Pirri, and Ray Reiter. Foundations for the Situation Calculus. Linköping Electronic Articles in Computer and Information Science, ISSN 1401<\#45>9841, Vol. 3(1998), Nr. 018.\r
+@ref:[12] Robin Milner, Mads Tofte and Robert Harper. The Definition of Standard ML. MIT Press, 1990.\r
+@ref:[13] S. Owre, N. Shankar, J. M. Rushby, and D. W. J. Stringer<\#45>Calvert. PVS Language Reference. Computer Science Laboratory, SRI International, Menlo Park, CA, September 1999.\r
+@ref:[14] J. Michael Spivey. The Z Notation: A Reference Manual. Second edition, Prentice Hall, 1992.\r
+@ref:[15] Ian Toyn et al. Formal Specification<\#151>Z Notation<\#151>Syntax, Type and Semantics. Consensus Working Draft 2.6 of the Z Standards Panel BSI Panel IST/5/<\#45>/19/2 (Z Notation). August 24, 2000.\r
+@ref:[16] Jim Woodcock and Jim Davies. Using Z: Specification, Refinement and Proof. Prentice Hall, 1996.\r
+@ref:[17] Jos Warmer and Anneke Kleppe. The Object Constraint Language: Precise Modeling with UML. Addison Wesley, 1999.\r
+@ref:[18] Pamela Zave and Michael Jackson. Conjunction as Composition. ACM Transactions on Software Engineering and Methodology II(4): 379<\#150>411, October 1993.
\ No newline at end of file
projects / IRC.git / blobdiff