Files in this item



application/pdf8127645.pdf (6MB)Restricted to U of Illinois
(no description provided)PDF


Title:Self-Checking Programs: An Axiomatic Approach to the Validation of Programs by the Use of Assertions
Author(s):Mili, Ali
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Computer Science
Abstract:The subject of this thesis is the development and investigation of a Methodology for program design and verification. The design part is described by a step-wise refinement process. The verification part is described by a set of Induction Rules. The distinguishing feature of this methodology is that it produces programs which are not proven to be correct but to have a property that 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 we can prove that any time it is executed on some input data and all assertions return True when they are checked for, then the output obtained is correct.
An example of design and verification of a self-checking program performing Gaussian elimination is shown. It is stressed that very little effort is needed for the verification of its self-checking property.
Issue Date:1981
Description:190 p.
Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1981.
Other Identifier(s):(UMI)AAI8127645
Date Available in IDEALS:2014-12-13
Date Deposited:1981

This item appears in the following Collection(s)

Item Statistics