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:

1975-09-01

Pagination or Media Count:

19.0

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