
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
Page Count:
22
Publication Date:
1992-01-01
ISBN-10:
0867586362
ISBN-13:
9780867586367
No comments yet. Be the first to share your thoughts!