Paul E. Black,
Is "Implementation Implies Specification" Enough?,
Conference on Theorem Proving in Higher Order Logics (TPHOLs'99),
Nice, France, (September 1999).
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
Get the paper in
Postscript (102k), or
This page's URL is /~black/Papers/tphols99.html
Wed Jul 10 10:27:53 2002
by Paul E. Black
Black's papers or
NIST home page.