> -----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
________________________________________________________________________


Reply via email to