Subject: Program Verification From: "William J. Rapaport" Date: Sat, 19 Sep 2009 14:59:47 -0400 (EDT) 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, i.e., to proving mathematically that a program is bug-free. 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 delimiters): 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.