Checking Consistency Between Source Code and Annotation

Abstract


We are able to check annotated code against tabular requirements using a tool called CORD. CORD uses annotations - comments inserted by the user as part of program documentation - and control-flow information to build its models. The models are later verified against tabular requirements. In order to use results of this verification, we have to convince ourselves that the code is properly annotated. This report describes a technique to check consistency between source code and annotations. Users specify correspondences between the requirements and the code variables directly, and our technique enables checking that these correspondences are preserved in the code. The report also describes a tool called SAC which implements this technique.