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.
- Computer Programming and Software