The assessment will involve writing a formal specification using the Z notation and then applying the ZTC type-checker. Once type-checked, you should attempt to use the ZANS animator on your specification. You should either use the example in Exercise 4 as a starting point or specify any system of your own choice. In the latter case, it is recommended that you choose a system that you already know well.

The specification should consist of the following as a minimum:

1. Definition of basic types.
2. Optional: axiomatic and/or generic definitions for use in the subsequent specification.
3. An abstract state schema.
4. An initial state.
5. Change of state schema if required.
6. At least three operations where success is assumed.
7. Success and error schemas providing suitable reports.
8. Definitions of total operations.
9. Optional: One or more validation hypotheses or theorems with proofs.

You are expected to do the following during the course of the term:

1. Produce a Z specification along the lines above, written in L^ATEX source form, and formatted using the L^ATEX document preparation system. Your formal specification should be accompanied by an informal explanation, of approximately the same size as the formal part of the description.

2. Successfully type-check the entire specification using the ZTC type-checker.

3. Attempt to animate part (at least one operation) of the specification using the ZANS animator. Note: make a separate copy of your specification for this since you will probably need to modify it to make animation possible. Any problems should be noted in your report.

You may discuss your specification with the demonstrator during practical sessions, or with the lecturer after the Monday lectures, as you develop it.

A report on your practical work during the term should be handed in at the end of the assessment period, covering the following:

1. Introduction to the problem which you decide to tackle.

2. Presentation of the Z specification, including matching informal English explanation.

3. Discussion of problems encountered in the development your specification, particularly with respect to ensuring its type correctness using ZTC.

4. Presentation of animation runs using ZANS for one or more operations in your specification.

5. Conclusions, including general problems encountered and any changes of approach you would use if you were to undertake the exercise again.

You may use the above items as the basis for the sections in your report. Feedback on your assessed work will be provided during the practical sessions and if required during lectures as well. You are expected to discuss your assessment as it progresses, as if you are a member of a design team.

It is highly recommended that you write up your report in draft form as you proceed, and polish it at the end, rather than leaving it all till the end.

Extra marks can be gained for the following:

• Elegance of specification and approach.
• Clarity and organization of your report.
• Simplicity (if correct), rather than verbosity.