Go backward to Simultaneous Definitions Go up to Top Go forward to Example

While Loops

C[[while B do C]] =
    fix(lambda f. lambda s. B[[B]]s -> f(C[[C]]s) [] s)

Function: Store_{_|_} -> Store_{_|_}

Example:

C[[while A>0 do (A:=A-1; B:=B+1)]]
= fix F where
    F = lambda f. lambda s. test s -> f(adjust s) [] s
    test = B[[A > 0]]
    adjust = C[[A:=A-1; B:=B+1]]

Partial function graphs:

• Each pair in graph shows store prior to loop entry and after loop exit.
• Each graph Fⁱ⁺¹(_|_) contains those pairs whose input stores finish processing in at most i iterations.