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 verification. 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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com