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 language | English (US) |
|---|---|
| Pages (from-to) | 155-160 |
| Number of pages | 6 |
| Journal | Information Processing Letters |
| Volume | 17 |
| Issue number | 3 |
| DOIs | |
| State | Published - Oct 5 1983 |
| Externally published | Yes |
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