CSSE 373 Formal Methods in Specification and Design

HW6

Purpose: practice designing Alloy models using the Event signature style

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. For this assignment you’ll be modeling the mailbox structure of an email client. Assume fixed mailboxes for incoming mail, outgoing mail, drafts of messages, previously sent mail, and deleted mail. Additional custom mailboxes may be arranged in a hierarchy. The beginning of a model for this system is given in hw06.als.

3. As in section 6.2.4 in the book, we’ll use events to model the email client, rather than operation predicates. The partial model hw06.als gives a few example events. For this part, your task is to complete the constraints for the following events:

   1. Create – begins a new message in the Drafts mailbox
   2. Send – Sends a message that is in the Outbox, files it in the Sent mailbox
   3. FileMessage – moves a message from one mailbox to another (besides Outbox, Sent, and Drafts)
   4. TrashMessage – moves a message to the Trash
   5. Rearrange – moves one custom mailbox into another

   Use the provided showEvent and showTrace commands to experiment with your events as you develop them. You should use Magic Layout, but that will hide the SpecialMailbox instances. To make them visible:

   • Click Theme
   • Click SpecialMailbox in the outline.
   • Make sure Show is checked in the properties above the outline.
   • While in the Theme editor, you may also find it useful to turn Show off for Events, but turn Show on for pre and post under Events.
   • Click Apply to see the results.
4. Finally, we want to verify that the constraints on our model hold. A couple of assertions are included in hw06.als, along with stubs for two more. Complete the assertions CustomMailboxesOK and MessagesOK by calling the appropriate (provided) predicates. Check that your model satisfies all the assertions, adding any necessary conditions to your events.
5. Bonus: Extend your model to include email filtering rules. Add appropriate signature(s) and events to represent such rules. Be sure to include predicates and assertions necessary to document the rules. (I haven’t tried this, which is why it’s a bonus problem. I suspect it will be challenging to do well!)
6. Be sure to document your model and include your name in the comments.
7. Turn in your work by committing both your Alloy model and a pdf file of your model to the appropriate HW folder in your homework team subversion repository for this course. Please make sure line wrapping in your pdf does not obscure your comments!