Harnessing a Refinement Theory to Compute Loop Functions

Ali Mili, Rahma Ben Ayed, Shir Aharon, Chaitanya Nadkarni

Research output: Contribution to journalArticlepeer-review

1 Scopus citations


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 languageEnglish (US)
Pages (from-to)139-155
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Jul 28 2009

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


  • Reverse engineering
  • program comprehension
  • program correctness
  • program semantics
  • refinement calculi
  • software maintenance
  • software tools
  • while loops


Dive into the research topics of 'Harnessing a Refinement Theory to Compute Loop Functions'. Together they form a unique fingerprint.

Cite this