Titolo del corso
Static and Dynamic Software Analysis
Codice identificativo del corso
1819-87R-SDSA
Extra practice with Alloy and the Alloy Analyzer
These exercises are optional and will not be corrected.
Exercise 1: Using the Alloy Analyzer to check an Alloy specification
Consider the Alloy specification for the address book given in the slides.
- Check the assertion noParentReflexivity; what’s the output? Is the assertion valid?
- Run the predicate personWithoutParents; what does the output mean? Is the predicate consistent with the specification? Which is the person without parents?
- Run the function personParents: the Analyzer will find an instance. What does this mean? Inspect the instance. What can you say about the specification now?
Exercise 2: Refining the Alloy specification with new facts
Add the following facts to the specification:
- Marriage is symmetric (x is married with y iff y is married with x)
- Marriage is irreflexive (noone is married with him/herself)
- A person is not one of his/her ancestors
- A person’s siblings are all and only the offsprings of at least one of her parents
- Incest, in the form of marriage between siblings or ancestors, is prohibited
fact f1 {Exercise 3: Check the consistency of the specification
all p: Person | _______________________________________________ _______________________________________________________________
}
fact f2 {
_______________________________________________________________ _______________________________________________________________
}
fact f3 { _______________________________________________________________ _______________________________________________________________
}
fun siblings[p : Person]: set Person { _______________________________________________________________ _______________________________________________________________
}
fact f5 {
no p: Person | ________________________________________________ _______________________________________________________________
}
Now that the specification contains many facts we may ask whether it is consistent. How do we check consistency? Write an assertion to check consistency and the check command to check it.
_______________________________________________________________ _______________________________________________________________ _______________________________________________________________ _______________________________________________________________ _______________________________________________________________ _______________________________________________________________ _______________________________________________________________ _______________________________________________________________
Check the consistency in the Alloy Analyzer. What result do you obtain? Comment its meaning. Now try to generate a number of unconstrained instances of the specification. Write a predicate and a run command that allows you to generate the instances.
_______________________________________________________________ _______________________________________________________________ _______________________________________________________________ _______________________________________________________________ _______________________________________________________________ _______________________________________________________________ _______________________________________________________________ _______________________________________________________________
Run it and inspect the instances. Have them the shape you expected? Is their number the right number?
Exercise 4: More predicates/facts
The following Alloy signatures are given:
sig Address { } sig Value {} sig Computer {
memory: Address -> Value } pred write[__________________________________________] {
________________________________________________________________
________________________________________________________________
________________________________________________________________
________________________________________________________________
________________________________________________________________ }
- Write an Alloy predicate for the memory write operation. This operation, given an Address addr and a Value val, modifies the memory of a computer at addr setting it to val. The content of all the other memory cells remains unchanged.
- Express the following assertion: In every computer’s memory, every memory address contains exactly one value.
- Later, we decide that the previous assertion is too strong for our needs. Precisely, we want that every address is associated to at most one value. Our idea is that addresses not associated to any value represent uninitialized memory cells. Suppose a nontrivial analysis scope for Address (say, 100): are there analysis scopes for Value not allowing the analyzer to find a counterexample to this last assertion?
Define a signature DeterministicFiniteStateMachine, defining a model for the structure (state and transitions) of deterministic finite state machines having:
- exactly one initial state;
- one or more final states;
- possibly some dangerous states;
- zero, one, or more transitions between states.
Write then a predicate named SafeComputation, which, given a DeterministicFiniteStateMachine m and a sequence of states seq, is true if and only if seq is a computation bringing m from its initial state to one of its final states, without passing for a dangerous state. At that scope you may use the module util/sequence[S] and the following declarations contained in it:
- sig Seq, whose atoms are the sequences of atoms of S
- sig SeqIdx, whose atoms are the indices of the sequences defined by Seq
- pred add[s: Seq, e: elem, s': Seq], true if and only if s' is obtained by appending e to s
- pred isEmpty[s: seq], true if and only if s is the empty sequence
- fun elems[s: Seq]: set S, returning the set containing all the elements of s
- fun inds[s: Seq]: set S, returning the set of all the indices of s
- fun first[s: Seq]: lone S, fun last[s: Seq]: lone S, returning the first/last element of s, or the empty set if and only if s is the empty sequence
- pred rest[s, s': Seq], true if and only if s' is the tail (i.e., the sublist starting after its first element) of s
- fun next[i: SeqIdx]: lone SeqIdx, returning the index (if exists)immediately after the index i
- fun at[s: Seq, i: SeqIdx]: lone S, returning the element of s at position i, or the empty set when s does not contain (i.e., is shorter than) i.
Ultime modifiche: giovedì, 19 settembre 2019, 19:04