CSE503: Software Engineering
Lecture 10  (January 27, 1999)

David Notkin


v     Formal specifications have several interesting properties

Ø      They can play at least two important and distinct roles

§        They can provide a basis on which to do verification, ensuring that an implementation indeed satisfies a specification (you "build the system right")

·        This is largely the basis for much of the work in program verification, which has not really succeeded to any significant degree

¨      But it’s the basis for a bunch of work in this area, and we will cover the basics today

§        They can be useful in increasing the confidence one has in the consistency and completeness of a specification

·        For example, consider the specification of an abstract data type: one can formally check that the specification of each operation on the ADT guarantees that invariants on the data itself are satisfied

§        There are also those who argue for "executable specifications"---that is, specs that can directly executed or easily translated to executable programs

·        This may work in some situations, but they are limited because there is a big gap between either

¨      the specification and the program (things that are easy to say in a specification are not necessarily easy to say in programs, especially efficiently --- negation and conjunction are simple examples)

¨      or else the user and the specification (reducing the utility of the specification for helping to ensure that you "build the right system")

Ø      We'll see some material on specifications based on logic/set theory, on algebra, on finite state machines

v     Proving programs correct

Ø      The basic premise here is that one starts with a specification and a program, with the job being to demonstrate that the program satisfies the specification

§        A closely related premise is that one can start with the specification and derive a correct program from it

Ø      Although there are many notations that can be used for this process, the two most well-known ones are Hoare triples and Dijkstra’s weakest preconditions (predicate transformers)

Ø      A Hoare triple is a logical predicate of the following form:

§        P {S} Q

·        A common variant is to write this as {P} S {Q}

§        P and Q are predicates, while S is a program

§        The meaning of P {S} Q is

·        If P is true and S executes

·        Then after S executes, Q is true

·        Assuming S terminates

§        The termination assumption makes this a proof of “weak correctness”

§        If termination is proven rather than assumed, then it becomes “strong correctness”

§        Ex:

·        true {y := x*x} y >= 0

·        x > 0 {x := x + 1} x > 1

·        x = X and y = Y {t := x; x := y; y := t} x = Y and y = X

¨      X and Y are constants

¨      Note that the final predicate is not as strong as it could be, since it could also include a conjunct t = X

·        x <> 0 {if x > 0 then x := x + 1 else x := -x} x > 0

§        These predicates depend on backsubstitution to capture the meaning of assignment

·        Consider the triple ? {x := exp} Q(x)

·        ? is the unknown precondition, Q is the postcondition that may be parameterized in terms of the program variable x

·        For Q(x) to be true afterwards requires that ? be equal to Q(exp) as a precondition

¨      Q(x) is defined as x > 1, meaning that Q(x+1) == x+1 > 1 == x > 0

¨      Q(y) == y >= 0 meaning that Q(x*x) == x*x >= 0 == true

·        This is handled technically by the proof rule

¨      B[a/X]{X:=a}B

¨      Where B[a/X] represents the predicate B with all free occurrences of X replaced by a

§        Ex of weak vs. strong correctness

·        x > 0 { y := f(x);
    function f(z : int): int is begin
        if z=1 return 1
        else if even(z) return f(z/2);
        else return f(3*z+1);
    end }
y = 1

·        I believe this function has been proven to return 1 if it terminates, but it is only a conjecture that it always terminates on positive integers

·        Therefore, this predicate is weakly correct, but not strongly correct

§        We'll come back to termination proofs, but I do believe that it is relatively rarely the case where termination is the central issue or problem with a program

·        Also, demonstrating non-termination is equally important for classes of programs, such as operating systems, avionics control systems, etc.

Ø      The basic approach to proving program correct using Hoare triples is as follows

§        One starts with the precondition (P), the postcondition (Q), and the program (S)

§        S usually consists of a sequence of statements

§        The person proving the program then introduces additional intermediate assertions between the statements

§        Ex:

·        P {S1;S2;S3;S4} Q

·        P {S1} A1 {S2} A2 {S3} A3 {S4} Q

§        Then prove each triple.  QED.

Ø      Technically, to do this requires some standard proof rules such as

§        If we can prove F1{S1}F2 and also F2{S2}F3 then we know that F1{S1;S2}F3 is true

§        If we can prove that F0 => F1 and the above, as well, we also know F0{S1;S2}F3

Ø      There are also proof rules for conditional statements, P{if C then S1 else S2}Q

§        If we can prove

·        P and C {S1} Q

·        P and not C {S2} Q

·        Then we have proven the triple P{if C then S1 else S2}Q

§        x <> 0 {if x > 0 then x := x + 1 else x := -x} x > 0

·        P == x <> 0
Q == x > 0
C == x > 0
x <> 0 and x > 0 == x > 0, so x>0{x:=x+1}x >0, which is trivially true
x <>0 and x <= 0 == x < 0, so x <0{x := -x}x > 0, which is also trivially true

Ø      Loops are the biggest challenge in proving correctness

§        One problem is proving termination; this is usually done separately from the proof about the program's computation

§        The other is that we have to introduce an added assertion, called a loop invariant, and these are not generally possible to compute, but rather have to be chosen carefully to allow the proof to go through

§        Consider the triple P{while C do S}Q

·        We need to find a loop invariant I and show the following properties

·        P => I                           //the invariant must be true when the loop starts

·        I and C{S}I                  //the invariant must remain true after each iteration

·        (I and not C) => Q        //if the loop terminates, the postcondition must hold

§        Trivial ex (from Ghezzi):

·        x >= 0 { while x>0 do x := x + 1 } x = 0
I == x >= 0
P => I trivially
x >= 0 {x := x+1} x >= 0 trivially
x >= 0 and x <= 0 => x = 0 trivially

Ø      Longer example:

i > 0 and j > 0

{t := i;

div := 0;

while t >= j do

    div := div+1;

    t := t-j;


i = div*j+t and 0 <= t < j


§        That is, divide i by j and put the quotient in div and leave the remainder in t.

§        In groups of 2-4, prove this correct, including explicitly identifying the loop invariant

v     An alternative formulation to Hoare triples is to use Dijkstra's weakest precondition predicate transformers that, in essence, provide a functional approach to handling the predicates

Ø      wp(Q,S) is defined to be the weakest logical predicate that must be true before executing S in order to prove that postcondition Q is true afterwards

Ø      Ex:

§        wp(x > 10,x:=x+1) = x > 9

§        wp(Q,skip) = Q

§        wp(Q,S1;S2) = wp(wp(Q,S2),S1)

§        wp(Q, if C then S1 else S2) = (wp(Q,S1) and C) or (wp(Q,S2) and not C)

Ø      In general, there is a direct analogy between Hoare triples and wp proofs, although on the whole, wp proofs seem a little more straightforward, as they seem to capture the intuitive notion of backwards reasoning for proofs more effectively