CSci 435/535: Homework 8

Formal Methods

Due by Monday, April 10th by 11am

Summary

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

There are several parts to this assignment:

1. Develop a formal specification in Alloy for hexes, arena, warriors, and obstacles. This should be a static (no time) model. Save this file as static.als.
2. Enhance your static model, creating dynamic.als. The dynamic model should add Time to the warriors. Specify the move-warrior operation, hard-coding the number of hexes that a warrior can move to be equal or less than 5.

You should not simply formalize the current implementation, but rather start over, thinking about how to represent the real world in an abstract way. Be sure to write any asserts for obvious invariants that should be true.

I do not expect you to formalize anything more than you need. i.e. Don't formalize hit points, weapons, etc.

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.

Submission

Email two files, static.als and dynamic.als, to csci435@coppit.org.

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.