Verifying programs by induction on their data structure: General format and applications

Research output: Contribution to journalArticlepeer-review

2 Scopus citations

Abstract

As a static object, a program presents two axes of complexity: the control structure and the data structure. The invariant assertion method is used to prove programs by induction on their control structure: The correctness of complex control structures is deduced from the correctness of their components, which are, in some sense, simpler. Orthogonally, one may want to prove programs by induction on their data structure: the correctness of the program on complex data items is deduced from its correctness on simpler data items. A general theorem of correctness by induction on the data structure is given. This theorem is applied with two distinct definitions of complexity (i.e., two distinct ordering relations on the space of the program) yielding, respectively, the subgoal induction method and the intermittent assertion method.

Original languageEnglish (US)
Pages (from-to)155-160
Number of pages6
JournalInformation Processing Letters
Volume17
Issue number3
DOIs
StatePublished - Oct 5 1983
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Signal Processing
  • Information Systems
  • Computer Science Applications

Keywords

  • Noetherian induction
  • Program verification
  • intermittent assertion method
  • subgoal induction method

Fingerprint Dive into the research topics of 'Verifying programs by induction on their data structure: General format and applications'. Together they form a unique fingerprint.

Cite this