Path: utzoo!attcan!uunet!tut.cis.ohio-state.edu!ucbvax!agate!agate!hughes From: hughes@lightning.Berkeley.EDU (Eric Hughes) Newsgroups: comp.software-eng Subject: Re: "Program Proving" Message-ID: Date: 22 Mar 90 14:30:38 GMT References: <1990Mar17.063012.24979@agate.berkeley.edu> <4389@stpstn.UUCP> Sender: usenet@agate.berkeley.edu (USENET Administrator;;;;ZU44) Organization: ucb Lines: 64 In-reply-to: cox@stpstn.UUCP's message of 21 Mar 90 22:26:26 GMT In article <4389@stpstn.UUCP> cox@stpstn.UUCP (Brad Cox) writes: Apparently you haven't heard that C (and its derivatives, including Objective-C and undoubtedly C++ as well) supports assertion checking. Please don't patronize me. Every single file of C code I write has "#include " in it. In fact, my own assert.h has a macro halt() in it to put in places where the code should never get to. Yes, it's useful. Yes, many people have not heard of it. Yes, it is my habit, almost a reflex. That's not the point. There are two big differences between using a runtime check (as in the assert() macro) and a compiler time check (an inline predicate asserted to be true). They are both called assertions, an unfortunate confluence which leads to misunderstanding. The first difference is entirely practical. There are some runtime checks which appear naturally in proof which just can't be realistically checked at runtime. Consider the behavior of the library routine malloc(). We want to be able to say that the pointer malloc() gives us points to a block of memory that is exclusively ours, that is, that there does not exist another pointer which will modify contents of this block. I do not know of a way to verify this with a runtime check. I do think it possible to prove a memory allocator correct with the above property, however. Here is another example, one where a runtime check cannot in principle be written. Pick any numerical algorithm that uses floating point numbers as an approximation to the real numbers, that is, that models a mathematical object by a computer one. We want to know what the maximum error is from any calculation, which leads naturally to terms of the form abs( f - r ), where f is floating point (a subset of the real numbers) and r is real. You can't evaluate this term on a computer. The second difference is much more important. I'll even assume, for the sake of this section of the argument, that any assertion can be checked at runtime, even the ones above. Even with this strengthening assumption, runtime checks do not provide use with the confidence of a formally correct program. For runtime checks only assure us that each single execution of the program is valid, not that every such possible execution will be. (Both these assurances presuppose that the compiler, operating system, hardware, etc., perform as expected. This is a different issue than Fetzer's article.) To say this in other language, runtime checking gives us enumerable instances of program execution; every time we run the program on a different input and it satisfies all of its assertions, we have another example of a correct execution of the program. On the other hand, when we make a logical proof that a program satisfies its preconditions and postcondition, we have assured ourselves (again, insofar as our models are correct) that the program will work correctly on every possible input; a formal proof gives us decidable instances of correct programs. The practical difference between these two is enormous. For a program which is checked for correctness at runtime is correct _only_ insofar as it is tested before release, but a program which is proved correct formally has the _further_ assurance that there is a logical and formal derivation of precondition and postcondition (and that is a powerful assurance in practice). Eric Hughes hughes@ocf.berkeley.edu