PROVING PROGRAMS BY STRUCTURAL INDUCTION: A NEW PERSPECTIVE ON THE SOMETIME METHOD AND THE SUBGOAL INDUCTION METHOD.

Research output: Contribution to journalArticlepeer-review

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 languageEnglish (US)
Pages (from-to)112-117
Number of pages6
JournalProceedings of the Hawaii International Conference on System Science
StatePublished - Dec 1 1983
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'PROVING PROGRAMS BY STRUCTURAL INDUCTION: A NEW PERSPECTIVE ON THE SOMETIME METHOD AND THE SUBGOAL INDUCTION METHOD.'. Together they form a unique fingerprint.

Cite this