Applied Formal Methods - Assessment 2
Part III Unit - 3/CS/7A

Lecturer: Jonathan Bowen

However, you should hand in an interim Z specification for inspection and comment during the first half of the term (by the lecture on Monday 23 February 1998 at the latest, but preferably earlier).

The assessment will involve writing a formal specification using the Z notation and then applying the ZTC type-checker, ZANS animator. The specification should then be rapid-prototyped using the Prolog logic programming language.

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 schemas.
6. At least two operations where success is assumed.
7. At least two error conditions.
8. Definitions of total operations.

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 (ideally at least one operation) of the specification using the ZANS animator. Any problems should be noted in your report.

4. Rapid-prototype part (ideally at least one operation) of the specification using the Prolog logic programming language.

5. Optional: Use the Z/EVES proof tool to check preconditions or do validation proofs on your specification.

You should discuss your specification with the lecturer during practical sessions, or before/after lectures, as you develop, animate, and rapid-prototype it. As a minimum, please see the lecturer and discuss your progress at the end of each of the stages above before proceeding to the next stage.

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. Discussion of problems encountered in development your rapid-prototype logic program, particularly with respect to ensuring that it matches your original specification. Use minimal program development to ensure the program runs at a reasonable speed and justify your development choices, at least informally.

6. Presentation of rapid-prototype runs using Prolog for one or more operations in your specification.

7. Optional: Report on your experiences using the Z/EVES proof tool, including details of any proofs attempted or completed.

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

9. List any references you used for the assessment. (See 3rd year project booklet for guidance on style.)

10. Include a copy of your Prolog rapid-prototype program as an Appendix, ensuring that suitable comments are included to make the program readable and to make it obvious how it matches the Z specification.

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.