CSci 435/535: Software Engineering

Homework 8: Formal Methods

Due by Monday, April 30th by midnight

Summary

Work in pairs on this assignment. Make sure the names of both students appear in the document.

Develop a formal specification in Alloy for a subset of our project. You must specify at least:

• The types User, Player, Team, and League.
• All necessary constraints on the types.
• Multiple leagues per user.
• The operations AddPlayerToTeam, DropPlayerFromTeam, MakePlayerActive and MakePlayerInactive. Specify these as predicates with primed variables indicating after states. (See the examples for a guide on how to do this.)
• Assertions for obvious invariants that should be true for your model.
• run and check statements so that I can view examples of your model and check your assertions.

You don't have to specify player positions, betting, attacks, matches, messages, or time. You should not simply formalize the current implementation, but rather start over, thinking about how to represent the real world in an abstract way. I do not expect you to formalize anything more than you need.

Writing the Specification

In terms of structure and exposition, your specification should contain comments that explain each bit of formalism, and should explain unformalized or abstracted aspects of the system.

Run alloy as ~coppit/bin/alloy. If you get errors in the message pane, you probably can't write to /tmp. Try running alloy on a different machine. If that doesn't work email me.

I've placed some examples of Alloy specifications at http://www.cs.wm.edu/~coppit/csci435-spring2007/homework/alloy-examples.zip. You should also take a look at the Alloy Quickstart (http://alloy.mit.edu/quickstart.php), Alloy Tutorial (http://alloy.mit.edu/tutorial3/alloy-tutorial.html, and Alloy Reference (http://alloy.mit.edu/reference-manual.pdf). Note that the latter two have not yet been updated for Alloy 4.

Bonus

Bonus points will be awarded for specifications that go beyond the above homework description to specify interesting, nontrivial aspects of the system. A minimal example is player positions. A substantial example is time, with a state machine that describes transitions resulting from operations.

Submission

Email your .als file to coppit@cs.wm.edu.

Grading

200 points total. Both team members earn the same grade. Bonus points will be awarded for specification of additional operations or interesting invariants. I will not award bonus points for merely specifying more attributes for the types.

You will be graded on completeness, correctness, structure/clarity, and appropriate structure and exposition.