Programming = Proving

From the examples that we have seen so far, it may appear that programming is as hard (and in fact the same type of activity) as proving a mathematical theorem. In a very abstract sense we can demonstrate this fact using NPPV.

Assume that X(n) is a property of natural numbers. X(n) is obviously true, if and only if a program P that starts at 0 and checks all numbers until it finds one that does not satisfy X, will never stop. In this abstract framework we can write the program P where the fact that P never stops can be specified by the postcondition False. Thus we obtain :

        { True }
          n := 0 ;
          WHILE X(n) DO 
            n := n+1
        { False }

NPPV will require us to annotate the loop with an invariant. Since it is not clear what this invariant should be, we just add an abstract predicate I(n), which may depend on n, the only variable in the program. The verification conditions that NPPV generates show very succinctly the connection between programming and theorem proving :

        I(0) 
        I(n) => I(n+1)
        I(n) => X(n).