> -----Original Message----- > From: [EMAIL PROTECTED] > [mailto:[EMAIL PROTECTED] > Behalf Of ljknews > Sent: 12 July 2004 14:24 > To: [EMAIL PROTECTED] > Subject: Re: [SC-L] Programming languages used for security > > > At 3:55 PM -0700 7/10/04, Crispin Cowan wrote: > > > However, I think I do see a gap between these extremes. You > could have > > a formal specification that can be mechanically transformed into a > > *checker* program that verifies that a solution is correct, > but cannot > > actually generate a correct solution. > > Isn't that pretty much what the SPARK Inspector does ?
Yes, the "posit and verify" approach. We adopted this because we think there are problems with refining specs into code. One problem is that there can be (usually will be) more than one valid way of implementing a spec. For example, the spec may make the abstract assertion that a list is "ordered". The implementation could build an ordered tree structure, write to a buffer that is periodically quicksorted or even write to a set of temporary files that are periodically merge sorted. The design choice may depend on non-functional requirements such as performance or amount of free memory. Therefore we don't see how you can always generate the most appropriate code for the property "ordered". One solution to this is to use very low-levels of specification that avoid the gap between the abstract concept ordered and the code itself. This can easily fall into the trap that the specification language simply becomes code (a problem with B for example). Our approach is to embed the property "ordered" as an annotation in the code , allow the designer to choose an appropriate solution and then provide facilities to show that the implementation preserves the required property. The SPARK Examiner generates the required proof obligations to do this. There is therefore clear blue water between the specification ("what") and the code ("how") but with a rigorous way of showing correspondence between them. Peter ________________________________________________________________________ This e-mail has been scanned for all viruses by Star Internet. The service is powered by MessageLabs. For more information on a proactive anti-virus service working around the clock, around the globe, visit: http://www.star.net.uk ________________________________________________________________________