On Tuesday 18 Sep 2012 00:00, Jon Lockhart wrote:

> 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 no longer myself involved in the use of Z or ProofPower 
in systems development.
My most recent use has been oriented towards philosophical 
rather than practical problems (and uses HOL rather than Z).

I was most closely involved in the application of formal 
methods to systems development (and in the development of 
ProofPower) between 1986 and 1994, and later collaborated 
with Rob on the ClawZ project.
During that time we used Z and HOL first with Cambridge HOL 
and then ProofPower on a number of projects mainly concerned 
with formal requirements analysis and high level design, for  
security critical or safety critical applications or for 
tools to support such developments.
None of these projects established a formal connection 
between the high level specifications and code, though one 
did verify a bit of hardware design to a low level.

The work in which specification and code were most closely 
related was possibly the ClawZ project, since the 
specification was written in a functional style and the 
implementation in Standard ML was able to follow the 
specification quite closely.  Of course this is not code 
verification, but it was a practical way of implementing a 
project in which there was no requirement for formal 

The most carefully worked out approach to the process of 
verified implementation against formal specifications in which 
we were involved is that on which the ProofPower Compliance 
tool was based, which is aimed at verified SPARK (Ada) code.
The documentation for this system is available from the 
lemma-one.com website.

Roger Jones

Proofpower mailing list

Reply via email to