Path: utzoo!utgpu!jarvis.csri.toronto.edu!rutgers!uwm.edu!zaphod.mps.ohio-state.edu!sol.ctr.columbia.edu!emory!hubcap!ncrcae!usceast!park
From: park@usceast.UUCP (Kihong Park)
Newsgroups: comp.theory
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <3048@usceast.UUCP>
Date: 14 Jan 90 16:48:10 GMT
References: <1891@uwm.edu> <1788@bruce.OZ>
Reply-To: park@usceast.UUCP (Kihong Park)
Organization: University of South Carolina, Columbia
Lines: 11

In article <1788@bruce.OZ> cjs@bruce.OZ (Chris Stuart) writes:
>In this discussion, it has been said that certain programs might resist
>proofs of correctness, because you can't solve the halting problem and
>thus there are programs for which you can't prove termination.

If one is looking for a general correctness checker then this statement is
true. But, in some instances(for whatever practical reason), one might
restrict the domain of the checking algorithm to programs which fall into
a well-defined subclass, e.g., the set of programs satisfying a certain
structural form. For such special subclasses, each subclass may very well
be a recursive set, hence the membership problem decidable.