Proving the LOOP function
We must demonstrate that our guess is good, i.e.
f = [WHILE]
= ( R < Y --> ident ) | ( R >= Y and Y > 0 --> Q,R := Q+R/Y, R mod Y )
- show f behaves like identity when the loop boolean is false
- show dom(f) = dom([WHILE])
Showing this involves a termination argument, since dom([WHILE])
is defined as all states such that the loop terminates when
executed in that state.
The loop obviously always terminates when R
When R>=Y it fails to terminate if Y<0 since R would increase each time
through the body.
So, dom([WHILE]) is ( R < Y or ( R >= Y and Y > 0) ).
From the definition of f, we see a clause to handle each disjunct of
the dom([WHILE]) expression.