Paul E. Black, Is "Implementation Implies Specification" Enough?, presentation to 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'99), Nice, France, (September 1999).

Abstract:

    An implementation is typically checked against a specification by proving that the implementation implies the specification. This ensures that the implementation only has behaviors allowed by the specification. However, this does not require the implementation to have any behavior at all!

    We propose that correctness statements have two parts, corresponding to liveness and safety. Safety is that the implementation implies an "allowed-behavior" specification, as now. Liveness is that a "required-behavior" specification implies the implementation.

Get the paper in DVI (16k), Postscript (102k), or PDF (129k).

This page's URL is /~black/Papers/tphols99.html

Updated Wed Jul 10 10:27:53 2002

Go to Black's papers or NIST home page.