Sciweavers

KBSE
1997
IEEE

A Formal Automated Approach for Reverse Engineering Programs with Pointers

14 years 3 months ago
A Formal Automated Approach for Reverse Engineering Programs with Pointers
Given a program S and a precondition Q, the strongest postcondition, denoted sp(S Q), is defined as the strongest condition that holds after the execution of S, given that S terminates. By defining the formal semantics of each of the constructs of a programming language, a formal specification of the behavior of a program written using the given programming language can be constructed. In this paper we address the formal semantics of pointers in order to handle a realistic model of programming languages that incorporate the use of pointers. In addition, we present a tool for supporting the construction of formal specifications of programs that include the use of pointers.
Gerald C. Gannod, Betty H. C. Cheng
Added 06 Aug 2010
Updated 06 Aug 2010
Type Conference
Year 1997
Where KBSE
Authors Gerald C. Gannod, Betty H. C. Cheng
Comments (0)