Anthony, Thank you very much for the information. It is information like that that has been missing from the documents I have been reviewing. I new it would be a difficult task and that there would be some discontinuity.
I will definitely take a look at your site and the papers you directed me towards. I have high interest in reading them. Thanks, Jon On Tue, Sep 18, 2012 at 5:31 AM, Anthony Hall <anth...@anthonyhall.org>wrote: > Jon**** > > ** ** > > 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 > http://anthonyhall.org/html/papers_on_formal_methods.html, 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**** > > ** ** > > Anthony Hall**** > > 22 Hayward Road**** > > Oxford OX2 8LW**** > > UK**** > > +44 (0) 7779 255147**** > > anth...@anthonyhall.org **** > > http://anthonyhall.org **** > > ** ** > > ** ** > > ** ** > > ** ** > > ** ** > > 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. > > Regards, > Jon Lockhart**** >
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
