CSSE 373 Formal Methods in Specification and Design

HW4

Purpose: practice refining a model to determine the correct pre-conditions for operations

This is a team homework assignment. All work must be done by the team members together. All team members should understand all work submitted. If you have concerns about your own understanding or that of your teammates, please let me know. I want everyone to learn all they can in this course!

1. 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.

2. Do exercise A.2.2 in Appendix A of the text. Some extra guidance:

   • You can avoid some initial typing by using File → Open Sample Model…, then navigating to book → appendixA → addressBook2.als.
   • Use File → Save As… to save your file as hw04_1.als in the HW4 folder of your Subversion working copy.
   • In the second line of the problem spec., the “viol” is extraneous. Just cross it out. (Meanwhile, some Renaissance Faire minstrel is singing a capella.)
   • For each part (a)–(f), put the code you used to find the answers in your model, clearly labeled with comments. Additionally:
     1. The invariant is described informally in the problem spec. Add comments to the invariant predicate, inv, in your model describing each constraint.
     2. Recall that you can use predicates within other predicates, so you can say things like inv[b] and not inv[b].
     3. You can define separate predicates to demonstrate add and del.
     4. You’ll change the scope of these checks later, so add comments indicating the smallest scope you used. You don’t have to give me your counterexamples, I just want your assertions in the model.

     5. Use your counterexamples generated in part (d) to decide what additional constraints you need to add.

        Note: When Jackson says “constraints on the prestates” he means constraints on b.addr, n, and t, but not on b'. It would be easy (in Alloy) to just say that the invariant must hold for b', but we're trying to discover what preconditions we would need if we actually implemented an address book.

        Justify your choice of scope for this part by adding a comment above each check command.

   • Commit your Alloy model to your repository.
   • Copy and paste your final Alloy model into your answers document.
3. If you want some additional practice, you could do exercise A.2.3. This is not required.
4. Be sure to document your models and include your names in the comments.
5. How much time did you spend on this assignment?
6. Turn in your work by committing a pdf file containing your answers to the appropriate HW folder in your homework team subversion repository for this course.