Proposals for Course Revision

1.	Replace Z in COMP2411 and COMP3111/9008 by B

1a.

Reasons for the proposal

Z is now used in all the above courses to give students an exposure to the use of formal methods in software development. "Formal methods" should be understood to mean, mathematically based with varying degrees of rigour through to formal proof.

The proposal to replace Z by B is aimed at replacing a specification notation by a more robust formal method whose application extends beyond specification through to implementation and beyond. This will give students a better appreciation of where the method can lead.

The proposed replacement of Z by B in these courses will not move substantially beyond specification, but it will, with the aid of the B Tookit to do a better job, and it should leave students with a clear view of where the method can take them.

1a1.

The current role of Z.

Z is now used in all the above courses to give students an exposure to the use of formal methods in software development. "Formal methods" should be understood to mean, mathematically based with varying degrees of rigour through to formal proof.

Z is really a specification notation. It is a very good one, it has a very nice flexible schema calculus, and it is still very much alive. But it is still only a specification notation.

1a2.

What is B?

The B method, usually abbreviated to B, is as its name suggests a method, not simply a notation. The method covers the software development lifecycle from specification through to implementation and maintenance. Z and B have a common author: Jean-Raymond Abrial. Both are based on logic and set theory, especially the relational calculus.

The components of a B development are called Abstract Machines: an encapsulation of a state and operations. A machine behaves like an object, but B does not support classes.

1a2a.

The phases of a B development

Specification: a formal definition of the required component or system expressed as an abstract machine. The definition may depend on other machines A B specification is a model of the required system.

Animation: a formal specification can be checked only for internal consistency; it cannot be checked for correctness, that is consistency with informal requirements for the system. The value of a specification ---formal or otherwise--- depends on how accurately it captures the requirements of the person who wants the system, the client. Animation is a technique for symbolically interpreting a specification so that the behaviour of the system can be checked against expectations.

Refinement: refinement is the name given to design in a formal setting. B supports a particular theory of refinement ---essentially that of the refinement calculus. In a refinement sequence a series of machines are produced. The machines contain more implementation detail, and in general have a different state, but the operations must have the same "effect". Refinements produce proof obligations, which should be discharged.

Implementation: an implement is a special, final refinement that produces an implementation machine. The implementation machine can be translated ---automatically by the B Tookit--- into code.

1a2b.

The B Toolkit

The B Method is supported by a toolkit, and the toolkit should be regarded as an indispensable part of the method.

The toolkit is a configuration manager that knows about the various phases of a development, and manages them. Some of the roles played by the toolkit are:

analysis: checking machines for various type of correctness. Checked machines are kept in a special directory and are reduced to a canonic form, for checking subsequent changes.

proof obligation generation: all proof obligations required by the theoretical foundations of the method are generated by the tool.

proof assistance: the toolkit supports a number of proof assistants (automatic and interactive) to help with the discharge of proof obligations.

code generation: implemented machines can be converted to code, currently C.

system library: a library of fully implemented machines that can be used for the implementation of your machines.

document generation and management: all aspects of the B development can be documented, and documents are subject to the same configuration management as other aspects of the development.

1b.

Proposed content of revised courses

All of the following would involve the use of the B Toolkit, so its role is not separated.

1) Mathematical toolkit: set theory and first order predicate calculus: essentially the same as for Z
2) Generalised Substitution Language and Abstract Machine Notation (AMN): replaces Z notation.
3) Specification: replaces Z.
4) Animation: no significant counterpart in Z. This is an important addition that will strengthen the students' understanding of requirements and specification.
5) Proof obligations and proof: replaces type checking for Z. A significant addition that should lead to a better understanding of the method and the production of "better" specifications.
6) An introduction to refinement: an overview of the whole process to make it clear where the method goes from here. Some fully developed case studies for demonstration purposes.
7) Examples of use in industry. A number of industrial case studies will be presented.

1c.	Subsequent study The course material in COMP2411, COMP3111/9008 would lead into, a possibly revised, COMP9116.

Split level 3 courses into 3uc courses.

While recently constructing example combined programs in SE/Math and SE/Physics, I was struck by the degree to which this exercise was aided by the availability of 3uc courses. The recent Physics revision consisted mainly of just that: the splitting of 6uc courses into two 3uc courses.

I have long believed that we should have smaller courses, especially in the later years.

There are a number of reasons why this is a "good idea"

1) Our programs are becoming more elective and less prescriptive. We should do things to make this process effective.
2) Students want to do a wide range of courses, smaller compact courses enable this.
3) There is strong interest in combined programs, and in multi-discipline study. We should help enable this.
4) We probably want to mount more courses ourselves. We have new staff and they will have their specialties in which they may like to mount courses. It doesn't make sense to have too many 6uc courses.
5) Teaching 3uc courses might lead to better teaching distribution.
6) There is nothing sacred about 6uc. Most, maybe not all courses can be condensed.

As an example, COMP3131 (Parsing and Translation) could be condensed to a 3uc course and a new 3uc course could be devoted to Compiling.