Author Description

Abstract: "A logical basis for correctness of implementations is proposed and its consequences discussed. The idea is to examine the relationship between the theory S of the specification and the theory I of the implementation. If S is contained in I then the implementation is adequate, and if I restricted to the language of S is contained in S it is safe. Adequacy turns out to be equivalent to the implementation being a model of S. Proper containment in adequacy implies implementation bias. Proof obligations in a well-known system of software verification are then shown to follow from the adequacy of the pre-condition predicate and the safety of the post-condition predicate