DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
Correctness Condition Graphs.
STANFORD UNIV CALIF DIGITAL SYSTEMS LAB
Pagination or Media Count:
A graphical, syntax-oriented method for computing and representing correctness conditions is proposed. For each flowchart program, a directed graph is generated which explicitly displays the structure and interrelationships among the antecedent, consequent, and verification conditions for its statements. The mapping of programs onto condition graphs is formally defined by augmenting the productions in a flowchart grammar with subgraph constructors. The goal is to give the programmer deeper insight into the semantics of his program, thereby facilitating his possibly interactive formulation of the assertions needed to carry out its verification.
APPROVED FOR PUBLIC RELEASE