Correctness Condition Graphs.
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1975
- Accession Number
- ADA017859
Entities
People
- Clifford R. Hollander
Organizations
- Stanford University