Three Kinds of Semantics

  - Operational (write an interpreter)
  - Axiomatic (list of axioms about what properties a fragment of code guarantees)
  - Denotational (formal mathematical meaning as function to each fragment of code)

  - Type Checking
    - fancy type systems can be used to encode & prove various correctness/safety
      properties

----------------------------------------------------------------

  Axiomatic Semantics, i.e., Hoare Logic

    - good for Partial Correctness
         Partial Correctness = NEVER GIVES WRONG ANSWER
	    (but might not always terminate)

	 Partially Correct + Always Terminates = Fully Correct


This is true:
   { true } i=1; while (i>0) do i := i+1 od { false }

valid inference rule:
   {Q} p {R}  &  {R} t {S}   =>    {Q} p;t {S}
that is what ';' means


Weakest Precondition: Q = wp(p,R) is the most general statement Q s.t. {Q} p {R}

  p is "i:=2*i"
  R is i>9

  Here are things S we could write such that {S} i:=2*i {i>9}

    i>1000000
    i>j & j>17
    i>3*x+4*y & x>0 & y>0 & x+y>100

  weakest precondition: i>4
    write wp(i:=2*i, i>9) = i>4

  weakest precondition must always exist, because ...
  {Q1} p {R} & {Q2} p {R}  =>  {Q1 or Q2} p {R}

     {wp(p,R)} p {R}

    (Q1 => Q   &  {Q} p {R}  &   R => R1)    =>    {Q1} p {R1}


LANGUAGE in use

   assignment statements
     STATEMENT ::= VAR := EXPR
     	       	   | STATEMENT ; STATEMENT
		   | skip
		   | abort
		   | if EXPR then STATEMENT else STATEMENT fi
		   | while EXPR do STATEMENT od

wp(p1;p2, R) = wp(p1, wp(p2, R))

  i.e., to find weakest Q s.t. {Q} p1;p2 {R}
       first find weakest Q1 s.t.  {Q1} p2 {R}
       then  find weakest Q  s.t.  {Q} p1 {Q1}

wp(skip, R) = R
wp(abort, R) = true (for partial correctness)
wp(abort, R) = false (for total correctness)

  inference rule for if statement:
   {Q & E} p1 {R}  &  {Q & not(E)} p2 {R}    =>   {Q} if E then p1 else p2 fi {R}

wp(if E then p1 else p2 fi, R) = 
      (E & wp(p1,R)) or (not(E) & wp(p2,R))
 or equivalently (?)
      (E => wp(p1,R)) & (not(E) => wp(p2,R))

Consider this:

  {Q} while E do S od {R}

inference rule for while loop

  when while loop terminates, postcondition is of form: not(E) & (something)

define a "loop invariant", L

  {E&L} S {L}   =>   {L} while E do S od {not(E) & L}

  {E&L} S {L}  &   ((L & not(E)) => Q)      =>   {L} while E do S od {Q}


Assignment

 example

    {j=0} i := j+1 {i=1}

 inference rule

    R does not contain any v   =>    {R} v := E {R}

 weakest precondition

    {R[v/E]} v := E {R}
    wp(v := E, R) = R[v/E]

   notation for substitution in expression:
      R[v/E] means substitute E for each v in R.

Example: factorial routine

objective: prove this:

   fact(n)
   begin
     a := 1;
     i := 1;
     while (i < n) do
       i := i+1;
       a := a*i
     od;
     return a
   end

annotate w/ what we want to prove:

   fact(n)
   begin
     {n >= 1}    // PRECONDITION
     { true }
     a := 1;
     i := 1;
     while (i != n) do
       i := i+1;
       a := a*i
     od;
     {a = 1 * 2 * ... * n}  // POSTCONDITION
     return a
   end

To prove:

     {n >= 1}
     a := 1;
     i := 1;
     while (i != n) do
       i := i+1;
       a := a*i
     od;
     {a = 1 * 2 * ... * n}

subproblem: find L s.t. L & not(i!=n) => a=1*2*...*n
   find L s.t.   L & i=n   =>   a=1*2*...*n
   L is a=1*2*...*i

  need to show:

     { (a = 1 * 2 * ... * i) & (i != n) }
       i := i+1;
       a := a*i
     {a = 1 * 2 * ... * i}

  and

   (a = 1 * 2 * ... * i) & not(i!=n)   =>   (a = 1 * 2 * ... * n)
     <=>
   (a = 1 * 2 * ... * i) & (i=n)   =>   (a = 1 * 2 * ... * n)
     <=>
   (a = 1 * 2 * ... * n)   =>   (a = 1 * 2 * ... * n)

   :TRUE

  to conclude:

     {a = 1 * 2 * ... * i}
     while (i != n) do
       i := i+1;
       a := a*i
     od;
     {a = 1 * 2 * ... * n}

  subsubproblem:

     (a = 1 * 2 * ... * i) & i!=n
      =>
     wp(i := i+1, wp(a := a*i, a = 1 * 2 * ... * i))
      ~=>
     wp(i := i+1, (a = 1 * 2 * ... * i)[a/a*i])
      ~=>
     wp(i := i+1, (a*i = 1 * 2 * ... * i))
      ~=>
     (a*i = 1 * 2 * ... * i)[i/i+1]
      ~=>
     a*(i+1) = 1 * 2 * ... * (i+1)

     :TRUE

 Now need to find

     {Q}
     a := 1;
     i := 1;
     {a = 1 * 2 * ... * i}

     Q = wp(a:=1, wp(i:=1, a = 1 * 2 * ... * i))
       = wp(a:=1, (a = 1 * 2 * ... * i)[i/1])
       = wp(a:=1, a = 1)
       = (a = 1)[a/1]
       = (1 = 1)
       = true

----------------------------------------------------------------

while loop, total correctness, inference rule

 partial correctness:
  {E&L} S {L}   =>   {L} while E do S od {not(E) & L}

 modify by adding a "loop variant", which is
   - non-negative integer
   - decreased each time through loop
   - going below 0 would end loop

 total correctness:
  {E & L & T=z} S {L & T<z}    &    L => (T>=0)
      =>   {L} while E do S od {not(E) & L}

For factorial while loop, would use loop variant: n-i

----------------------------------------------------------------

   binary search(n, a[n], x, &t)
     { EXISTS(x,a) & SORTED(a) }
     mi := 0;
     ma := n-1;
     while (mi < ma) do
       i := mi + (ma-mi)/2;
       if (a[i] < x) then mi:=i
       else if (a[i] > x) then ma:=i
       else if (a[i] = x) then mi:=i; ma:=i
       fi
     od
     t=mi;
     {a[t] = x}

abbreviations:
 EXISTS(x,a,lo,hi) = (exists j, s.t. lo <= j < hi & a[j] = x)
 SORTED(a) = forall j, s.t. 0<=j<n-1, a[j]<=a[j+1]

----------------------------------------------------------------

   binary search(n, a[n], x, &t)
     { EXISTS(x,a,0,n) & SORTED(a) }
     {S1}
     mi := 0;
     {S2}
     ma := n;
     {S3}
     while (mi < ma-1) do
       {L}
       i := mi + (ma-mi)/2;
       if (a[i] < x) then mi:=i
       else if (a[i] > x) then ma:=i
       else if (a[i] = x)
              then mi:=i; ma:=i+1
       fi
     od
     {S4}
     t:=mi;
     {a[t] = x}

L =  EXISTS(x,a,mi,ma) & SORTED(a)

S4 = wp((t:=mi), (a[t] = x))
   = (a[t] = x)/[t/mi]
   = (a[mi] = x)

S3 = L

subgoals:

 to prove while loop (partially) correct:

(w1)   S3 => L

(w2)   {L & mi < ma-1}
       body-of-while-loop
       {L}

(w3)   L & not(mi < ma-1) => S4

w3:
  EXISTS(x,a,mi,ma)
   & SORTED(a)
   & not(mi < ma-1)
  => (a[mi] = x)

  ==>

  EXISTS(x,a,mi,ma)
   & SORTED(a)
   & mi = ma-1
  => (a[mi] = x)

  but there is only one such j ...

  (check)

w2:

   {EXISTS(x,a,mi,ma)
    & SORTED(a)
    & mi < ma-1}
   body-of-while-loop
   {EXISTS(x,a,mi,ma)
    & SORTED(a)}

   (a is const, can remove from post)
   (expand loop body)

   {EXISTS(x,a,mi,ma)
    & SORTED(a)
    & mi < ma-1}
       i := mi + (ma-mi)/2;
       if (a[i] < x) then mi:=i
       else if (a[i] > x) then ma:=i
       else if (a[i] = x) then mi:=i; ma:=i+1
       fi
   {EXISTS(x,a,mi,ma)}

   (use weakest precondition stuff)

   (EXISTS(x,a,mi,ma)
     & SORTED(a)
     & mi < ma-1)
   =>
   wp((i := mi + (ma-mi)/2;
       if (a[i] < x) then mi:=i
       else if (a[i] > x) then ma:=i
       else if (a[i] = x) then mi:=i; ma:=i+1
       fi),
      EXISTS(x,a,mi,ma))

   (start expanding wp(...))

   (EXISTS(x,a,mi,ma)
     & SORTED(a)
     & mi < ma-1)
   =>
   wp((i := mi + (ma-mi)/2),
      wp((if (a[i] < x) then mi:=i
          else if (a[i] > x) then ma:=i
          else if (a[i] = x) then mi:=i; ma:=i+1
          fi),
      EXISTS(x,a,mi,ma)))

   (EXISTS(x,a,mi,ma)
     & SORTED(a)
     & mi < ma-1)
   =>
   wp((i := mi + (ma-mi)/2)
      ,
      (a[i] < x) & wp(mi:=i, EXISTS(x,a,mi,ma))
      or
      (a[i] > x) & wp(ma:=i, EXISTS(x,a,mi,ma))
      or
      (a[i] = x) & wp(mi:=i; ma:=i+1, EXISTS(x,a,mi,ma)))

   (EXISTS(x,a,mi,ma)
     & SORTED(a)
     & mi < ma-1)
   =>
   wp((i := mi + (ma-mi)/2)
      ,
      (a[i] < x) & EXISTS(x,a,i,ma)
      or
      (a[i] > x) & EXISTS(x,a,mi,i)
      or
      (a[i] = x) & EXISTS(x,a,i,i+1))

   (EXISTS(x,a,mi,ma)
     & SORTED(a)
     & mi < ma-1)
   =>
    (a[mi + (ma-mi)/2] < x) & EXISTS(x,a,mi + (ma-mi)/2,ma)
    or
    (a[mi + (ma-mi)/2] > x) & EXISTS(x,a,mi,mi + (ma-mi)/2)
    or
    (a[mi + (ma-mi)/2] = x) & EXISTS(x,a,mi + (ma-mi)/2,mi + (ma-mi)/2+1))

----------------

  S2 = wp(ma:=n, S3)
     = wp(ma:=n, EXISTS(x,a,mi,ma) & SORTED(a))
     = EXISTS(x,a,mi,n) & SORTED(a)

  S1 = wp(mi:=0, S2)
     = wp(mi:=0, EXISTS(x,a,mi,n) & SORTED(a))
     = EXISTS(x,a,0,n) & SORTED(a)

  EXISTS(x,a,0,n) & SORTED(a) => S1

 QED

-----------------------------------
Digression: non-deterministic if,
if
 TEST1 -> BODY1
 TEST2 -> BODY2
 TEST3 -> BODY3
fi

----------------------------------------------------------------
Axiomatic Semantics: WRAPUP

(1) don't specify what code *does*, but rather what it *promises* to make true

(2) {precondition} code {postcondition}
    means: is precondition is true and code runs then postcondition will be true

(3) partial vs total correctness

(4) two kinds of "proof steps"
    (a) derivation rules
         - sometimes require "creativity", e.g., figure out loop invariant
    (b) weakest precondition
         {wp(C,R)} C {R}
         - can be done mechanically
         - but no nice closed form for wp((while ...), R)
         - but there are for all non-loopy constructs

----------------------------------------------------------------
Make up some weird language constructs, and accompanying Axiomatic Semantics

   maybe C    (means system might execute code C or might not.)

   derivation rule:
     {Q} C {R}  &  Q=>R     ==>    {Q} maybe C {R}

   wp case:
     wp(maybe C, R) = R & wp(C, R)

   ----
   test_and_set(v,old,new)
     - like: if v=old then v:=new
       but works w/ threads

   could translate to:   if v=old then v:=new

   ----
   exceptions ...

   ----
   in_some_order(C1,C2)      means execute C1;C2 or C2;C1

   derivation rule
     {Q1} C1;C2 {R}  &  {Q2} C2;C1 {R}    ==>   {Q1 & Q2} in_some_order(C1,C2) {R}

   weakest precondition
     wp(in_some_order(C1,C2), R) = wp((C1;C2),R) & wp((C2;C1),R)

   ----
   get ideas from Haskell list comprehensions?
   [ 1..7 ] = [1,2,3,4,5,6,7]
   [ x*x | x<-[1..7] ]
   [ 1000*x+y | x<-[0..9], y<-[0..9] ]

   search
     x in X
     y in Y
   s.t.
     T

    (idea: finds x in X and y in Y s.t. T holds, sets them to those
    values, if none such exists aborts)

    (1) could rewrite as nested loops
    (2) left as exercise: come up with derivation rule(s) & wp for this construct,
        for both partial & total correctness