SELF-CHECKING PROGRAMS: AN AXIOMATISATION OF PROGRAM VALIDATION BY EXECUTABLE ASSERTIONS.

Gernot Metze, Ali Mili

Research output: Contribution to conferencePaperpeer-review

1 Scopus citations

Abstract

The subject of this study is the development and investigation of a methodology for program design and verification. The design part is described by a process of step-wise refinement of the specifications of the program. The verification part is described by a set of HOARE-like Induction Rules. The distinguishing feature of this methodology is that it produces programs which are not proven to be correct but have a property which is weaker than correctness: The Self-Checking Property. The Self-Checking Property is based on a systematic use of assertions and is defined as follows: A program is said to be Self-Checking if and only if it is proven that any time it is run on some input data and all assertions are TRUE when they are cheked, then the output computed for that particular input is correct.

Original languageEnglish (US)
Pages118-120
Number of pages3
StatePublished - Jan 1 1981
Externally publishedYes
EventDig Pap FTCS 11, Annu Int Symp on Fault-Tolerant Comput, 11th - Portland, ME, USA
Duration: Jun 24 1981Jun 26 1981

Conference

ConferenceDig Pap FTCS 11, Annu Int Symp on Fault-Tolerant Comput, 11th
CityPortland, ME, USA
Period6/24/816/26/81

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'SELF-CHECKING PROGRAMS: AN AXIOMATISATION OF PROGRAM VALIDATION BY EXECUTABLE ASSERTIONS.'. Together they form a unique fingerprint.

Cite this