{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/66455"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/66455","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Self-Checking Programs: An Axiomatic Approach to the Validation of Programs by the Use of Assertions","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Mili, Ali"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2014,"date_issued":"2014-12-13T18:02:23Z","date_published":"2014-12-13T18:02:23Z","updated_at":"2026-07-22T22:25:56Z","subjects":["Computer Science"],"languages":["eng"],"rights":[],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["(UMI)AAI8127645"],"render_values":[{"text":"(UMI)AAI8127645","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2142/66455","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Mili, Ali"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2014-12-13T18:02:23Z","10000-01-01","1981"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/66455","(UMI)AAI8127645"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Made available in DSpace on 2014-12-13T18:02:23Z (GMT). No. of bitstreams: 1 8127645.pdf: 5574677 bytes, checksum: 980d13d5e7196d33521a12e64c4b5413 (MD5) Previous issue date: 1981","Embargo set by: Seth Robbins for item 66633 Lift date: Forever Reason: Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","U of I Only","190 p.","Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1981."]},{"key":"dc:title","label":"Title","values":["Self-Checking Programs: An Axiomatic Approach to the Validation of Programs by the Use of Assertions"]}]}],"canonical_facts":{"dc:creator":["Mili, Ali"],"dc:date":["2014-12-13T18:02:23Z","10000-01-01","1981"],"dc:description":["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.","Made available in DSpace on 2014-12-13T18:02:23Z (GMT). No. of bitstreams: 1 8127645.pdf: 5574677 bytes, checksum: 980d13d5e7196d33521a12e64c4b5413 (MD5) Previous issue date: 1981","Embargo set by: Seth Robbins for item 66633 Lift date: Forever Reason: Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","U of I Only","190 p.","Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1981."],"dc:identifier":["http://hdl.handle.net/2142/66455","(UMI)AAI8127645"],"dc:language":["eng"],"dc:subject":["Computer Science"],"dc:title":["Self-Checking Programs: An Axiomatic Approach to the Validation of Programs by the Use of Assertions"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:56Z"}