Abstract
As a static object, a program presents two orthogonal dimensions of complexity: The control structure and the data structure. As a dynamic object, a program presents two more dimensions: Trace of execution (sequence of labels reached during execution) and the length of execution (number of iterations executed). This paper presents the general format of program verification by induction on the data structure and considers some well-known applications of it.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 112-117 |
| Number of pages | 6 |
| Journal | Proceedings of the Hawaii International Conference on System Science |
| State | Published - 1983 |
| Externally published | Yes |
All Science Journal Classification (ASJC) codes
- General Computer Science