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 language | English (US) |
|---|---|
| Pages | 118-120 |
| Number of pages | 3 |
| State | Published - 1981 |
| Externally published | Yes |
| Event | Dig Pap FTCS 11, Annu Int Symp on Fault-Tolerant Comput, 11th - Portland, ME, USA Duration: Jun 24 1981 → Jun 26 1981 |
Conference
| Conference | Dig Pap FTCS 11, Annu Int Symp on Fault-Tolerant Comput, 11th |
|---|---|
| City | Portland, ME, USA |
| Period | 6/24/81 → 6/26/81 |
All Science Journal Classification (ASJC) codes
- General Engineering