CSSE 373 Formal Methods in Specification and Design

HW3

Purpose: practice writing expression using the Alloy logic

Keep track of how much time you spend on this assignment. You will submit your answers as a pdf file at the end of the homework.
Do exercise A.1.4 in Appendix A of the text. Some extra guidance:
- In Alloy 4, type scopes don’t limit the number of Int instances. To be able to create smaller counterexamples, use the following template model rather than that provided in the text:
```
// Problem A.1.4
module homework/hw3_1

sig Thing {}

assert union {
  all s: set Thing, p, q: Thing->Thing |
    s.(p+q) = s.p + s.q
}
check union for 4
```
- For parts (a)–(c), if the identity doesn’t hold, give your counterexample by giving the three relations s, p, and q. (You can read these from the picture in the visualizer if you reduce the scope enough.)
- Copy and paste your final Alloy model into your answers document.
Do problem A.1.5 in Appendix A of the text. Again, some extra guidance:
- Use the following template model rather than that provided in the text:
```
// Problem A.1.5
module homework/hw3_2

sig Node {}

pred isTree[r: Node -> Node] {
  ...
}

run isTree for 4
```
- To write your constraints, consider what properties you need to express. How many root nodes does a tree have? Which nodes can you reach starting with the root? How many parents do non-root nodes have? I found it helpful to write these properties down as comments in my Alloy model before trying to write them as Alloy constraints.
- Copy and paste your final Alloy model into your answers document.
Do problem A.1.10. Clearly label (using a comment) each invariant and simulation constraint that you add.
- Read constraint (b) as “All names (in the domain of the address relation) eventually map to an address.”
- Add an additional invariant, “Aliases must directly map to at most one address or name.”
- For parts (e)–(h) copy and paste the Alloy expressions from the Alloy evaluator into your answers document.
- Also, copy and paste your final Alloy model into your answers document.
Turn in your work by committing a pdf file containing your answers to the appropriate HW folder in your individual subversion repository for this course.
Please complete the short, anonymous survey on ANGEL regarding this assignment. (I will study these surveys in detail after the conclusion of this offering of the course. If you have suggestions that you would like me to consider during this offering of the course, please tell me in person or use the separate Anonymous Suggestion Box on ANGEL.)