Browse Prior Art Database

A NEW INCOMPLETENESS RESULT FOR HOARE.'S SYSTEM

IP.com Disclosure Number: IPCOM000128019D
Original Publication Date: 1975-Dec-31
Included in the Prior Art Database: 2005-Sep-14
Document File: 12 page(s) / 28K

Publishing Venue

Software Patent Institute

Related People

Mitchell Wand: AUTHOR [+3]

Abstract

A structure is presented for which Hoare's formal system for partial correctness is incomplete, even if the entire first- order theory of A is included among the axioms. The implications of this result for program-proving are discussed.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 22% of the total text.

Page 1 of 12

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

A NEW INCOMPLETENESS RESULT FOR HOARE.'S SYSTEM

Mitchell Wand Computer Science Department Indiana University Bloomington, Indiana 47401

TECHNICAL REPORT No. 35 A NEW INCOMPLETENESS RESULT FOR HOARE'S SYSTEM MITCHELL WAND JULY, A New Incompleteness Result for Hoare's System

Mitchell Wand*

Abstract

A structure is presented for which Hoare's formal system for partial correctness is incomplete, even if the entire first- order theory of A is included among the axioms. The implications of this result for program-proving are discussed.

Key Words and Phrases

Program proving, Program correctness, partial correctness.

CR Categories

5.24, 4.22, 4.6

Authorls.address: Computer Science Department, Indiana University, Bloomington, Indiana 4,7401.

1. Introduction

In [41, Hoare introduced a formal system for the derivation of statements about the partial correctness of programs. A number of results on the incompleteness of this and similar systems are well known, falling into two.major categories:

(1) termination incompleteness. It is easy to build structures A and B which have the same first- order theory and a program P which is total on A and nontotal on B Thus there can be no complete calculus of termination based only on first-order formulas.

(2) recursive incompleteness. Since most interesting structures have nonrecursive theories, their partial correctness theory is likewise nonrecursive. With slightly more.care, it may be shown that the set of partial correctness assertions true in every structure is not recursive [71.

Indiana University Page 1 Dec 31, 1975

Page 2 of 12

A NEW INCOMPLETENESS RESULT FOR HOARE.'S SYSTEM

In subsequent work on program correctness, difficulty (1) has been avoided by using calculi of partial correctness. Difficulty (2) has been ameliorated by attempting to build finite but.useful catalogs of facts about the structures to be manipulated, or by relying o n,an automatic or interactive theorem prover to prove the verification conditions generated in the course of a program proof.

In this paper we will show that this device cannot succeed. We will give a structure A and an assertion P{SIQ which is true in A but is not provable in Hoare's system even if we admit as an axiom every first-order sentence.which is true in A We argue that the difficulty is not Hoare's system but the choice of the first-order predicate calculus as a specification language. Along the way we show that difficulty (1) never appears for partial correct- ness calculi. Last, we compare our results with those of Cook E21 and consider the implications for practical program proving.

I

2. Preliminaries

Let w denote the non-negative integers 0,1,2,... For the remainder of this section assume that all sets of symbols are dis- joint. A similarity type T consists of

(Equation Omitted)

where

PS and CS are sets (of function symbols, predicate symbols, and constant symbols respectively) and rank...