CSci 420/520: Homework 6

Alloy Analyzer Orientation

Due Friday, October 21st by 1pm.

Summary

Alloy is a modeling language developed by the Software Design Group at MIT. Its associated tool is the Alloy Analyzer. In this assignment, you will set up the required Alloy environment and take a first peek at the Alloy language.

Make sure you have Alloy running as described in the tools setup document.

Before doing this assignment, you might want to do the quick tutorial from the Alloy website (http://alloy.mit.edu/quickstart.php).

The Alloy Analyzer takes a different approach from PVS. Instead of providing powerful theorem-proving tools to help you prove your model is correct, it instead "simulates" your model and tries to find counterexamples. The existance of counterexamples indicates that your model has inconsistencies. This approach greatly simplifies matters for the user, since you don't have to develop a proof. However, the tool does not actually prove a model is correct. It can only claim that the model may be valid. To gain more confidence that the model is correct, you can increase the scope, which increases the size of the instances that the Alloy Analyzer checks.

Assignment

1. Download birthday_book.als and place it into your work directory.
2. Start the Alloy Analyzer and open birthday_book.als.
3. Above each function and assertion, write a comment that explains briefly (yet precisely!) what it means.
4. Typecheck the model. You should not see any error messages
5. Execute all the check and run statements. These will be found in the dropdown box.
6. Answer the following questions and store them in a file called homework6.txt. Do this using your favorite text editor.
   1. Why does BusyDay generate an example? What is wrong with it?
   2. The check DelIsUndo yields an example. Explain in simple English what the example is saying. You should use the state diagrams and the text explanations to help you.
   3. Briefly explain why checking AddRemind with different scopes gives you different answers.
7. Change the DelIsUndo assert to fix the problem mentioned above.
8. Change the AddRemind assert to fix the problem mentioned above.

Grading

150 points total.

Email homework6.txt and your modified birthday_book.als to meghan@cs.wm.edu.