In this chapter, we briefly introduce the modeling language named Alloy that we use throughout the thesis.
2.1 What is Alloy?
Alloy is a modeling tool which is developed by MIT Professor Daniel Jackson and his research group. The latest version of Alloy is Alloy 3.0-bata. Alloy can model data structure, such as abstract data type which is the basis of OO programming. Alloy model checker has two properties (1) Satisfiability (SAT) [10] check. (2) 1st order predicate logic
2.2 Basic Syntax of Alloy 2.2.1 File Name and Path
Every alloy file is name as file_name.als .In each file, the first part of the program begins with the path of the file, for example,
module models/research/alloy/file_name If user needs to include other file (maybe utility file, test file, marco library etc …), he can use the “ open “ file function , for example: open util/boolean .Once we open the file, we can apply all the declared sets, functions which are included in the file(in the example is boolean.als and bolean.als is located under the folder util)
2.2.2: Sets, Subsets and Relation
Set is the basic component of the program, and it is declared as:
sig Human{}, sig represents signature which tells the alloy that “Human” is a set.
Users can use the key word “ in “ or “extends” to declare some set(s) is(are) a subset of the other, for example: sig Men in Human{} , which means book is a subset of Object .The difference between in and extends is that extends partitions the sets and all the subset extends the set are disjoint, for example,
sig Men extends Human{}
sig Women extends Human{} :
It means Men and Women partition the set Human and the subset Men and Women are disjoint and their union is the set Human. But if we write
sig Men in Human{}
sig Women in Human{}
, it doesn’t mean Men and Women partition Human and their union is the set Human. In alloy,
everything is a relation, such as unary, binary and ternary relation. In the braces, users can define relation .For example:
sig Human{ eat : some Food , beLoved : set Human }
eat is a relation mapping from Human to Food which means “Every human being eats food.”
and beloved is a relation maps Human to Human that means “Every Human being has zero or more human being like this Human”. Here we apply multiplicity key words some (one or more) and set (zero or more) .We will introduce multiplicity markings in the next section.
2.2.3: Multiplicity
In Alloy, the following are the multiplicity key words.
lone: less than or equal to one one: exactly one
some: one or more set: zero or more all: all
If a user what to declare there’s only one element in the set, he can write “one sig Book {}”. From the previous sector, if we rewrite “sig Book extends Object{} , sig Pen extends Object{}” into” one sig Book extends Object{} one sig Pen extends Object{}”, it means the two subset Book and Pen both have only one element in it and the set Object only has two elements. Multiplicity marking can be used in set declaration, fact, predicate, function, assertion. We will introduce fact, predicate, function, assertion in the following section.
2.2.4: Fact
Facts are the constraint statements that always hold through out the simulation and verification process. Every model has its own specification and according to the specification, we apply the specification into the fact for Alloy to generate all cases under the constrain statements of fact. According to the listed-fact statement, Alloy uses it for simulation and verification. For example,
fact { some h: Human | h.beLoved = none}:
It means there are some human being(s) that no one loves.
2.2.5 Predicate and Function (a)Predicate
If all the inputs satisfy the listed constraints, then the predicate will be be true.
pred loveTest (m:Men , w:Women){ w in m.beLoved},
It means giving two input argument m which belongs to Man and w which belongs to Women.
If the w loves the m, the predicate returns true otherwise returns false. Predicate has another function. When it comes to simulation, the listed statement in the brace will be combined (conjoint) with all the fact listed in the program and generate one of the instances satisfies all the constraints statement.
(b) Function
Function can be used to simulate like the Predicate does and it has another function which can be used to return a set of element satisfying the listed statement in the brace (which is it body). For example,
fun loveSet (m:Men , W : set Women ) : set Women{ m.beLoved & W}:
It which means giving a m belongs to Men and a set of Women and according to the input set W, function loveSet returns the set of women Who love the m. Here “&” means intersection.
2.2.6 Run, Assert and Check
After a user declare all sets, relations, facts, functions and predicates, he can use the command “run” to simulate one of cases which meets constraints. For example,
run loveSet for 10 Human:
It will generate one of the instances under the scope of 5. Users only specify the scope for top level signature. What is top level signature? It’s the set that doesn’t extend other sets.
Here in our example, Human is the top level signature .Since Men and Women extends Human, these two are not top level signature. The command “run” is used for simulation, and the command “check” is used for verification. When a user makes an assertion, he would like to know if the assertion stands or not. That is the command “check” used for. For example, assert famousPeople {some m: Men | m.beLoved = Women }
check famousPeople for 10:
We make an assertion “famousPeople” that in every case, there’s at least one man that every women loves. We check the assertion under the scope of 10.
2.2.7 Further References
If reads are interested in understanding more about alloy, please refer to the main page : http://alloy.mit.edu [1] it’s reference manual [2] for further acknowledgement .