Formal Semantics for Program Paths

Lermer, Karl, Fidge, Colin and Hayes, Ian J. (2003). Formal Semantics for Program Paths. In: James Hartland, Electronic Notes in Theoretical Computer Science. CATS'03, Computing: the Australasian Theory Symposium. Computing: The Australasian Theory Symposium [CATS], Adelaide, (58-81). 4-7 February 2003. doi:10.1016/S1571-0661(04)81006-5

Author Lermer, Karl
Fidge, Colin
Hayes, Ian J.
Title of paper Formal Semantics for Program Paths
Conference name Computing: The Australasian Theory Symposium [CATS]
Conference location Adelaide
Conference dates 4-7 February 2003
Proceedings title Electronic Notes in Theoretical Computer Science. CATS'03, Computing: the Australasian Theory Symposium   Check publisher's open access policy
Place of Publication Amsterdam ; New York
Publisher Elsevier Science
Publication Year 2003
Sub-type Fully published paper
DOI 10.1016/S1571-0661(04)81006-5
ISSN 1571-0661
Editor James Hartland
Volume 78
Start page 58
End page 81
Total pages 24
Collection year 2003
Language eng
Abstract/Summary This paper provides the syntax and semantics for a systematic approach to the problem of analysing control-flow paths in computer programs. We give an abstract syntax and a partial correctness semantics for program control-flow paths as a generic model for path analysis and constraint derivation. This approach is formally based on a predicate transformer semantics over a boolean-valued predicate space and an abstract command language. The notions of a command, dead commands, the entry and exit conditions of a command and the inverse of a command are formally defined and investigated on the base of the semantics. A notion of command refinement is introduced capturing the abstraction process in program development from specification to implementation with partial correctness. Furthermore, command-reduction theorems and characterisations for command refinement are derived using the underlying semantics. Finally we verify the equivalence of weakest liberal precondition and strongest postcondition semantics for program commands in terms of the ordering relation they define on the command language. The approach is generic in that it is applicable to any program language that can be supplied with a predicate transformer semantics
Subjects 080309 Software Engineering
Keyword Control-flow path analysis
partial correctness semantics
path refinement
weakest liberal precondition semantics
Strongest postconditions
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status UQ

Version Filter Type
Citation counts: Scopus Citation Count Cited 4 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Thu, 08 Jan 2009, 15:32:14 EST by Maryanne Watson on behalf of School of Information Technol and Elec Engineering