------------------------------------------------------------------------
Subject:  Program Verification
------------------------------------------------------------------------

Here is a nice use of predicates and propositional functions in computer
science:  to "verify" programs, i.e., to logically prove that a program
is correct.

E.g., consider the "swap" procedure (which I will write in a pseudocode
that should be pretty self-explanatory; I will use ":=" as the
assignment operator, and I will use braces "{" and "}" as comment
delimieters):

	procedure swap (x,y)
	begin
	  temp := x;
	  x := y;
	  y := temp
	end

To verify this program, i.e., to prove that it is correct, i.e., to
prove that it really will swap the values of its input, we want to make
sure that if x = a and y = b *before* the swap, then x = b and y = a
*after* the swap.  I will use logical propositions as comments to
illustrate this:

	{x = a ^ y = b}
	temp := x;
        x := y;
        y := temp
	{x = b ^ y = a}

In other words:  If (x=a ^ y=b) is true before the swap is executed, and
if the swap is then executed, then (x=b ^ y=a) should be true after the
swap is executed.

The proof of this can be shown by a series of comments after each line
of the program:

        procedure swap (x,y)
        begin
	  {x = a ^ y = b}
          temp := x;
	  {x = a ^ y = b ^ temp = a}
          x := y;
	  {x = b ^ y = b ^ temp = a}
          y := temp
	  {x = b ^ y = a ^ temp = a}
        end

These comments, expressed as propositions (actually, as propositional
functions, because they contain variables), show the state of the
computer before and after each statement of the program is executed,
and, because the last comment logically implies what we wanted to prove,
namely, that x = b ^ y = a, it verifies the program.

To learn more about this, see Rosen, Sect. 4.5, and the bibliography at
http://www.cse.buffalo.edu/~rapaport/584/S07/canprogsbeverified.html
or take CSE 451.