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.orgwrote:
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
