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
