Abstract
We consider a while loop on some space S and we are interested in deriving the function that this loop defines between its initial states and its final states (when it terminates). Such a capability is useful in a wide range of applications, including reverse engineering, software maintenance, program comprehension, and program verification. In the absence of a general theoretical solution to the problem of deriving the function of a loop, we explore engineering solutions. In this paper we use a relational refinement calculus to approach this complex problem in a systematic manner. Our approach has many drawbacks, some surmountable and some not (being inherent to the approach); nevertheless, it offers a way to automatically derive the function of loops or an approximation thereof, under some conditions.
Original language | English (US) |
---|---|
Pages (from-to) | 139-155 |
Number of pages | 17 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 243 |
DOIs | |
State | Published - Jul 28 2009 |
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- General Computer Science
Keywords
- Reverse engineering
- program comprehension
- program correctness
- program semantics
- refinement calculi
- software maintenance
- software tools
- while loops