This is a very large question!


The answer depends on the nature of your system design. There needs to be,
in addition to the specification, a description of the structure of your
implementation. Now there are two broad cases to consider:

1. ("Specifying in the small") For small systems it may be that the
structure of your implementation closely matches the structure of your
specification. That is, a module (say a subsystem) in your specification is
implemented as a module in your code.

2. ("Specifying in the large") For realistic systems there is a huge gap
between the structure of the specification and the structure of the code. No
part of the Z specification is matched by a single part of the
implementation. The implementation may consist of many processes on
different machines, using middleware such as databases, that don't appear in
the specification at all.


In the first case then you can proceed more or less formally. The fully
formal route would use something like the refinement calculus to develop
your program in a provably correct way from your specification. The less
formal route (the only one I have actually used, but it can be effective) is
to write a set of programming rules that say how each Z construct is mapped
into code. For example you would define, for the various kinds of set in
your specification, the corresponding implementation structure. 


In the second case you need a major design step that defines how the state
in your specification is mapped to the states of the various subsystems in
your design, and how each operation in your specification is implemented,
typically as a complicated transaction across the various subsystems in your
design. You can use, for example, UML sequence diagrams (or better-defined
alternatives like live sequence charts) for the latter. I don't think you
can really do this formally yet for realistic systems.


For a couple of examples of how this has been done in practice for large
systems see the papers on my website at, particularly
Correctness by Construction: Developing a Commercial Secure System, Anthony
Hall and Roderick Chapman, IEEE Software Jan/Feb 2002, pp18-25 and Using
Formal Methods to Develop an ATC Information System,Anthony Hall, IEEE
Software, March 1996, pp 66-76.


Hope this helps




Anthony Hall

22 Hayward Road

Oxford OX2 8LW


+44 (0) 7779 255147 






Dear Community,

I had a discussion with my adviser today on an inevitable step we will have
to take after these proofs of my specifications are complete and that is to
take the specification and use it to write code for the system. This is
because of course the specification only tells us what the system does, not
how it should be performed, as when you code there may be many ways to
achieve a goal even with system constraints. In all the documentation that
we have read so far, when someone mentions they have taken their
specification have developed the system from it, no matter what the
language, they usually state that there was no need to check the code since
the specification was proven correct initially and therefore there are no
errors, or they just gloss over the details saying they did it with no real
discussion on how or what problems they ran into. Of course these two areas
are a simplification but most can fall under one of these two from what we
have read.

In any case, we came up with the question of what do you do when you are
taking the specification and developing the code from it? So, I thought
since many of you have written specifications in Zed like I am doing now,
what have you all done to take the system specification that you have
developed and implement that system in code? 

I am really interested in what everyone has to say and their experiences.

Jon Lockhart

Proofpower mailing list

Reply via email to