Path: utzoo!attcan!uunet!snorkelwacker!apple!agate!agate!hughes From: hughes@tempest.Berkeley.EDU (Eric Hughes) Newsgroups: comp.software-eng Subject: Re: "Program Proving" Message-ID: Date: 19 Mar 90 16:44:16 GMT References: <1990Mar17.063012.24979@agate.berkeley.edu> Sender: usenet@agate.berkeley.edu (USENET Administrator;;;;ZU44) Organization: ucb Lines: 162 In-reply-to: bks@alfa.berkeley.edu's message of Sat, 17 Mar 90 06:30:12 GM In article <1990Mar17.063012.24979@agate.berkeley.edu> bks@alfa.berkeley.edu (Brad Sherman) writes: > I still think that it would be interesting to see a proof so I'll > try once more: Your original question was whether the included routine was correct or not. The answer, without looking at the code itself, is no, for the simple reason that code, _per se_, is not proven correct. What is proven is the code plus its precondition and postcondition. Since there is no precondition and no postcondition, the code cannot be proven to do anything. Now, here is what these conditions are. This is not the formal definition, but a working description. The notation generally used is {P} S {R}; here P is the precondition, S is the statement (which may be a compound statement or subroutine), and Q is the postcondition. P and Q are logical predicates (a predicate is a sentence that is either true or false) which describe program state. {P} S {R} is said to be correct if, when P is true at the beginning of the execution of S, then R is always true and the end of execution of S. Here is a simple example: {true} a = 1 { a equals 1 } Here the precondition is the true predicate. Every program state satisfies the true predicate. The statement is the assignment of the value one to the variable a. The postcondition asserts that the value of the variable a is 1. The program is correct, we reason informally, since if you assign the value one to a, then the value of a is one. This may seem rather silly, but there is a fundamental principle here: statements and predicates alternate, each statement moving the current assertion about program state forward one step. I think that a proper statement of preconditions and postconditions is one of the best debugging tools. I recently had too maintain a 500 line section of 8086 assemby code which was basically undocumented. The first thing I did was to triple the size by adding assertion, postconditions, and preconditions everywhere. In testing, I was able to fix half a dozen bugs simply by comparing the stated postcondition of a routine to the expected precondition of some statement and observing that the previous postcondition did not imply the precondition. It was truly wonderful. Without going into too much detail, I have written a proof of the given subroutine and augmented the code with it. I would say that this is a different program, myself, even though the individual code statements were unaltered. Don't worry if you don't understand some of the constructions, we can discuss them. For more details, go get a copy of _The Science of Programming_, by David Gries, from which I learned how to do this. The proof is as complete as I think a hand checked proof needs to be; in fact, I think it overly verbose. (Every proof is, by nature, verbose.) It is also not _really_ complete. I left out a calculation to show that the bound function is always greater than zero. This proof took about an hour to write. Eric Hughes hughes@ocf.berkeley.edu /* --------------------------------------------------------------------- * RXUTOS * RadiX Unsigned TO String. * Author: Bradley K. Sherman (bks@alfa.berkeley.edu) * With thanks to: Freek Wiedijk (freek@fwi.uva.nl) * Copyright (C), The Regents of the University of California, 1990 */ /* Precondition: * 2 <= radix <= 36 * n > 0 * the length of the representation of n in base radix is not greater * than RXUTOS_BUFFER_SIZE * Postcondition: * return value points to a ASCIIZ string which is a representation of * the number n in base b. */ /* Define b = radix */ char * rxutos( n, radix ) register unsigned int n; register unsigned int radix; { #define RXUTOS_BUFFER_SIZE 10 static char buf[ RXUTOS_BUFFER_SIZE + 1 ]; char *s = RXUTOS_BUFFER_SIZE + buf; *s = '\0'; /* Assert s is the empty string. */ /* Define: let t be the length of the representation of n in base b * Define: let s' be the number represented by s in base b * Define: let u be a loop counter, starting at zero * Define: n' = n */ /* Assert s' == 0 * Assert s' + n * 1 == n' * Assert n = [ n' / 1 ] */ /* Invariant: * s' + n * b^u== n' * n = [ n' / b^u ] // real division, greatest integer function * s is an ASCIIZ string * buf == s + RXUTOS_BUFFER_SIZE - u * Bound function: * t - u * Guard: * n > 0 */ do { /* Define s'' = s' * Define n'' = n */ --s; /* Assert buf == s + RXUTOX_BUFFER_SIZE - (u + 1) * Assert u <= t - 1 // from the bound function > 0 * Assert u >= 0 * Hence Assert s in buf[0..RXUTOS_BUFFER_SIZE+1) * Note: this is necessary because with a language * that allows pointers to point anywhere there is * a need to explicitly show that a derefenced pointer * assignment is permitted. */ *s = "0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZ"[n % radix]; /* Assert s is still an ASCIIZ string * Assert s' = s'' + ( n'' mod b ) * b ^ u * Assert n > 0 */ n /= radix; /* Assert n >= 0 * Assert n == [ n'' / b ] * == [ [ n' / b^u ] / b ] * == [ n' / b^(u+1) ] */ /* Assert s' + n * b^(u+1) * == s'' + (n'' mod b) * b^u + [ n''/b ] * b^(u+1) * == s'' + b^u * ( n'' mod b + b * [ n''/b ] ) * == s'' + b^u * n'' * == n' */ /* Stmt ++u * Assert buf == s + RXUTOX_BUFFER_SIZE - u * Assert n == [ n / b^u ] * Assert n >= 0 * Assert n' == s' + n * b^(u+1) * Assert bound function has decreased by one * Note: I have not shown that the bound function * is greater that zero after the guards. */ } while ( n > 0 ); /* Assert n >= 0 and not n < 0 * Assert n == 0 * Assert n' == s' + 0 * b^u == s' * Assert s is the representation of the input n in base b */ return( s ); } /* --------------------- End of file rxutos.c --------------------- */