Accession Number : ADA017859
Title : Correctness Condition Graphs.
Descriptive Note : Technical note,
Corporate Author : STANFORD UNIV CALIF DIGITAL SYSTEMS LAB
Personal Author(s) : Hollander,Clifford R.
Report Date : SEP 1975
Pagination or Media Count : 19
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.
Descriptors : *Computer programming, *Syntax, Semantics, Grammars, Mathematical logic
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE