The follows details a foreshadowed course revision and a suggestion 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 subjects 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 subjects 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 subjects 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 subject material in COMP2411, COMP3111/9008 would lead into, a
possibly revised, COMP9116.
2. Split level 3 subjects into 3uc subjects.
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 subjects. The recent Physics revision
consisted mainly of just that: the splitting of 6uc subjects into two 3uc
subjects.
I have long believed that we should have smaller subjects, 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 subjects, smaller compact subjects
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 subjects ourselves. We have new staff
and they will have their specialties in which they may like to mount
subjects. It doesn't make sense to have too many 6uc subjects.
5) Teaching 6uc subjects might lead to better teaching distribution.
6) There is nothing sacred about 6uc. Most, maybe not all subjects can
be condensed.
As an example, COMP3131 (Parsing and Translation) could be condensed to a
3uc subject and a new 3uc subject could be devoted to Compiling.
Ken Robinson
9 September 1999