I. developing loops, an introduction (Cohen's chapter 8)
 A. before and after
  1. other forms of postconditions
  2. establishing the invariant
 B. steps
---------------------
   INVARIANCE THEOREM FOR LOOPS

 {P} do B -> S od {P /\ !B}
  <==  {P /\ B} S {P}	        (Invariance)
    /\ {P /\ B /\ t==T} S {t<T} (Progress)
    /\ P /\ t<=0 ==> !B         (Boundedness)
----------------------
  1. invariant choice and initialization
---------------------------------------------------------
  STEPS IN DEVELOPMENT OF LOOP

0. choose invariant P and guard B
   so that P /\ !B ==> R
1. Develop S0 to establish P, i.e. find S0
   so that {Q} S0 {P}
---------------------------
 C. the loop body
	what would you choose for t if P is 0 <= i and B is i > 1?
--------------------
   FINISHING STEPS

2. choose bound function, t, such that
	P /\ (t <= 0) ==> !B
3. develop loop body S to satisfy
  a. invariance {P /\ B} S {P}
  b. progress {P /\ B /\ t == T} S {t < T}
--------------------
  1. summary
-----------------
  ANNOTATED FORM OF TYPICAL LOOP {PROOF}

 {Q}
 S0
 {invariant P, bound t}
 ; do B -> {P /\ B /\ t = T} S {P /\ t < T} od
 {P /\ t <= 0, hence P /\ !B, hence R}
---------------------------------------------------------
 D. remarks
II. developing loops (Cohen's chapters 9-10)
 A. heuristic 1: deleting a conjunct (chapter 9)
-------------
   HEURISTIC 1 FOR CHOOSING INVARIANT

(deleting a conjunct):
 if postcondition R is a conjunction,
 then delete
      the most difficult to truthify.

(what's most difficult?):
  conjunct that gives enough info
  for solution (i.e, part of answer)
--------------
  1. integer division example (9.1)
----------------
  EXAMPLE (INTEGER DIVISION)

  var x,y: int {Q: 0<=x /\ 0<y}
; var q,r:int
; q,r: (R:0<=r /\ r<y /\ q*y+r == x)
-----------------
   a. choose invariant
-----------------
0. choose invariant and guard
    invariant, P: 0<=r /\ q*y+r == x
    guard: r>=y,
------------------
   b. establish invariant
----------------
1. establish invariant
    {Q:  0<=x /\ 0<y}
    q,r := 0,x
    {P}
-----------------
	check that wp.(q,r := 0,x).P <== Q?
   c. choose bound function
------------------
2. choose bound function
	let bound function be r
------------------
   d. develop loop body
---------------
3. develop loop body
   solve for K>0 and E in
   {P /\ (r>=y)} r,q := r-K,E {P}
---------------
	why does boundness hold?
  2. linear search example (9.2)
----------------
   EXAMPLE (LINEAR SEARCH)

  var x: int {0 <= X /\ f.X}
; x: (R: 0 <= x /\ f.x
      /\ (\forall i : 0 <= i /\ i < x : !f.x))
-----------------
	can you develop this?  What are the steps?
  3. avoid avoidable case analysis (9.3) (omit)
  4. postpone design decisions (9.4) (omit)
 B. replacing constants by fresh variables (chapter 10)
-------------------
   HEURISTIC 2 FOR CHOOSING INVARIANT

(replace constants by fresh variables):
 If the postcondition has the form
	x == f.N,
 then rewrite it as
	x == f.n /\ n == N
 and choose
	invariant: x == f.n
	guard: !(n == N)

(constrain fresh vars to ensure defined):
 If f is partial, 
	and defined on (i:0<=i<M)
 then choose
	invariant: x == f.n /\ (0<=n<M)
	guard: !(n == N)
----------------------
---------------------------------------------------------
          EXAMPLE (10.2) THE MINIMUM VALUE

 var b: array of int {#b > 0}
; var x: int
; x : (R: x == (\min i : 0 <= i /\ i < #b : b.i))

 where \min is not allowed in the program.
---------------------------------------------------------
	what constant can you eliminate?
        What constraints are needed?
  1. accumulators (10.2, 10.4, 10.5)
---------------------------------------------------------
                    ACCUMULATORS

Assume P0: x == (\min i : 0 <= i /\ i < n : b.i),
       P1: 0 <= n /\ n <= #b
   and G: n != #b

    wp.(n,x := n+1, E).P0
==   {definition of P0, assignment}
    E == (\min i : 0 <= i /\ i < n+1 : b.i)
==   {arithmetic}
    E == (\min i : 0 <= i /\ i <= n : b.i)
==   {arithmetic}
    E == (\min i : 0 <= i /\ (i < n \/ i == n) : b.i)
==   {predicate calculus}
    E == (\min i : (0 <= i /\ i < n) \/ (0 <= i /\ i == n) : b.i)
==   {splitting the range}
    E == ((\min i : 0 <= i /\ i < n : b.i)
          min (\min i : 0 <= i /\ i == n : b.i))
==   {by assumption P0}
    E == x min (\min i : 0 <= i /\ i == n : b.i)
==   {Leibnitz}
    E == x min (\min i : 0 <= n /\ i == n : b.i)
==   {by assumption P1}
    E == x min (\min i : i == n : b.i)
==   {one-point rule}
    E == x min b.n
---------------------------------------------------------
  2. strengthening the invariant (10.4, 10.5)
  3. maintaining an invariant by constraining the allowed operations (10.7)