Quotient Program: Proof Plan

The spec r is

The program P is
    Q := 0
    R := X
    while R>=Y do
       Q := Q + 1
       R := R - Y
    end
We will decompose this as
    [Q:=0] o [R:=X] o [WHILE]
Steps:
  1. find [WHILE]
    1. guess function f such that f = [WHILE]
    2. use Mills' theorem to verify your guess:
      1. show ( ~b --> f ) = ( ~b --> identity )
      2. show dom(f) = dom([WHILE]) (a termination argument)
      3. show f = [IF] o f where IF is composed of loop components

  2. determine the restriction on [WHILE] made by the initial assignments to get [P]
  3. show that the program implements the spec, i.e., r subset [P]