Topics on Axiomatic Semantics
- off by one errors
- program proofs
- assertions (e.g., the assert keyword in Java JDK 1.4, 1.5)
- loop invariants
- Motivation for Axiomatic Semantics
- Basic Examples, Assignment, If-Then-Else.
- Design by Contract

Motivation
- Mission Critical Software
  - prove program does what it's supposed to
- What's Java's assert any good for?
  - run-time vs. design-time correctness
- If initial conditions are met (guarantee) contractually agree to produce
  certain result

In this example:
- Postcondition is supplied, so the goal is to figure out a
  reasonable precondition
  - What do we mean by "reasonable"?

- Remember, in Java...
  - assert requires a boolean expression
  - evaluated at run-time
  - if the assert expression evaluates FALSE at runtime an
    exception is thrown/raised

- What precondition(s) will ensure the postcondition is true after the
  two assignment statements are executed?

  Example Preconditions - which ones work? which don't? which are "better"?:
  - x == 1 and y == 2 and 
  - x == 1 and y == 5
  - y == 2
  - y < 200

Motivation for "WEAKEST" precondition
- Weakest means most permissive, i.e., most possible initial
  conditions of variables -- or most possible scenarios that would
  yield a TRUE evaluation of the boolean expression

- Another way to think about WP: what are the minimal requirements (in
  this case, for foo's initial parameter values) to ensure that the
  postcondition will pass (i.e., evaluate TRUE)

- Note, an alternative way to prove correctness is based on STRONGEST
  postcondition, which is not presented.

Q: SO WHAT IS THE BEST WP FOR THIS EX.?

GENERAL RULE:
 - substitute LHS with RHS.
 - works for assignment statements
 - note this can be extended for other situations:
   - parameter passing
   - return values
   - multiple value assignments, for example   x,y,z := 1,4+v,u;

In Java, sometimes written/documented as:

    /**
     * PRE: ...
     * POST: ...
     *
     * @param ...
     *//
    void foo(int x, y, z) {
      ...
    }

In Java, alas, this is just documentation.
Eiffel supports pre/post assertions enforced by the compiler.  Example:

    foo (x, y, z: INTEGER) is 
            -- Some wordy comments...
        require 
            (PRECONDITION EXPRESSION GOES HERE)
        do 
            ... (body of the function goes here)
        ensure
            (POSTCONDITION EXPRESSION GOES HERE)
    end

This is also known as "Design by Contract"


Another example:
IF-THEN-ELSE Statement

- As before postcondition is supplied as given; must determine WP

  int lo;
  assert ( fill this in... );    // PRE
  if (x < y) {
    lo := x;
  } else if (x > y) {
    lo := y;
  }
  assert (lo == min(x, y) );   // POST

Put in an assert statement before and after every Java statement.

  int lo;
  assert ( ... );   //1
  if (x < y) {
    assert ( ... );   //2
    lo := x;
    assert ( ... );   //3
  }
  else if (x > y) {
    assert ( ... );   //4
    lo := y;
    assert ( ... );   //5
  }
  assert (lo == min(x, y) );  //6

Method:
 - copy assert expression from //6 to //5 and to //3

 - using the assignment rule, substitution work backwards through
   else-body, if-body

 - then using general rule for IF STMT, //1 should look like this

  assert( (x<y) => //2  and  (x>y) ==> //4)

asserts inside elseif-body:

     assert (y == min(x, y));   //4

assert inside if-body:

     assert (x == min(x, y));   //2

simplifying //1, we get

((x < y) ==> x==min(x,y)) and ((x > y)==> y==min(x,y))

simplifying,

- At this point we recognize we found a missing case that our program
  didn't handle, so we need an else case to handle (x==y)

Q: after fixing the program, adding another else clause, what will the WP be?


Note: The notation used for WP examples in most texts doesn't use Java.
Three big differences worth noting:

(1) Curly braces surround boolean expressions instead of using assert clauses
    But then, this is a just syntactic sugar difference, anyway.

(2) If statements use "guarded commands" e.g.,

    if (x<y)  ->  statements  
    [] (x=y)  ->  statements  
    [] (x>y)  ->  statements  
    fi

    Not just syntactic sugar.  Unlike Java, all test expressions
    (known as guards) eval'd first, then randomly
    (non-deterministically -- esp. with the do..od loops we'll see
    soon) select a true guard to "fire"

(3) With Java assert statements the emphasis is on execution, but with
    WP the emphasis is on mathematical manipulation: don't care about
    how the program runs, but concerned with its correctness.  Thus
    the programs are not viewed for what they do when executed, but
    are viewed for how we manipulate them symbolically when juxtaposed
    with boolean expressions.  Once the general rules for WP are
    known, solving for a WP given a postcondition and some programming
    code, is like solving a high school algebra problem.

    Specifically,

      { bool expr }  CODE  { bool expr }

    Can be simplified to another

      bool expression

    Note that now there are no curly braces, no code, and that its
    just an expression.

       { true }  x := 3  { x==5 }

    Can be simplified to false.

       { y==5 } if (y>1) then x := y else y := x  { x==5 }

    Simplifies to true.

A Discipline of Programming: a Characterization of Semantics by EWD.
  - EWD == Ed (Edsger) Wybe Dijkstra - important CS pioneer - died in 2002
  - Wrote lots of important things about programming languages
    including the famous article, "Go To Statement Considered
    Harmful", 1968 Communication of the ACM

The Science of Programming by David Gries, Springer-Verlag, 1981.
  - David Gries has written a very good Discrete Mathematics text, which
    may include some WP and loop invariant information, and a popular
    compiler construction text and a bunch of other books.
  - Johnny thinks Gries writes and explains things really well,
    e.g., his science of programming is a much easier read than dijkstra's
    discipline