Specification-to-Code Correlation

System Development Corporation (SDC) has developed an informal approach for establishing correspondence (or lack thereof) between the formal specifications of a system and lower levels of specification, including implementation code. Establishing correspondence means showing that one level meets the intent of a higher lever. This paper presents the motivation, technique, and current SDC experience with the method, contains an example of the hypothetical correlation analysis, and evaluates the limits and the usefulness of this approach. This paper results from recent applications of the method.