that the completeness of testing can be measured structurally in terms
of source code. The testing only validates the specified property, using
the property’s specification to guide dynamic analysis of the program.
Information derived from the specification determines which points in