DocumentCode :
3233749
Title :
Deriving verification conditions and program assertions to support software inspection
Author :
Powell, Daniel
Author_Institution :
Sch. of Comput. & Inf. Technol., Griffith Univ., Australia
fYear :
2002
fDate :
2002
Firstpage :
447
Lastpage :
456
Abstract :
In order to trust a reusable software component, the correctness of its implementation with respect to its specification must be assured. Formal proof of correctness, while offering this assurance, is an often difficult, if not impractical, goal to achieve. Formal code reading techniques employed in software inspection have proved useful as a human reasoning process to verify correctness with a high degree of assuredness. Such techniques rely on the reader being able to abstract the semantics of a given component in order to reason about its correctness. The paper presents a method and supporting tools which yield formal semantic properties directly from the syntax of the component´s code. The method includes an extension of existing algorithmic and heuristic invariant generation techniques. Although, in many cases, the semantic information derived is strong enough to be useful as program assertions in Hoare-style formal proofs, we focus on the generation of information to assist human reasoning based code reading processes. To this end, we use examples to illustrate the application of the method and prototype tools to yield semantic information directly from program code, such as first-order predicate calculus specifications, input-output diagrams, and constructive reports of loop termination conditions.
Keywords :
program control structures; program verification; software reusability; Hoare-style formal proofs; constructive reports; correctness; first-order predicate calculus specifications; formal code reading techniques; human reasoning based code reading; input-output diagrams; loop termination conditions; program assertions; reusable software component; semantic information; software inspection; syntax; verification conditions; Inspection; Software engineering;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Engineering Conference, 2002. Ninth Asia-Pacific
ISSN :
1530-1362
Print_ISBN :
0-7695-1850-8
Type :
conf
DOI :
10.1109/APSEC.2002.1183016
Filename :
1183016
Link To Document :
بازگشت