FIXED POINT AND INVARIANT In their discussion of Axiomatic Semantics Programming

Language textbooks give an approach to handling assignment and decision statements which is straightforward. Consideration of simple unnested whiles and the invariants necessary for their proof however is not straightforward. What is required of an invariant is clearer, than what it is. Here we explore the assertion that an invariant for a while is equivalent to the fixed point of a related recursive definition. Those tail-recursive definitions equivalent to whiles in a program that have fixed points can usually be represented as assignments. Where it is possible to replace a simple while in a Program P with an assignment statement, proof of the consequence of larger parts programs may become feasible. Relation Of Recursion And while A recursive definition consists of a set of conditioned equalities. Each equality is asserted to hold under a condition involving the relation of its parameters. The fixed point of a recursive function definition, R, is a function, gfp(X) (X is a set of parameters) which satisfies the equalities of R. The object of including the recursive definition facility in a programming language in which a desired function, gfp(X), is not directly available, is to be able to realize gfp(X). The programmer usually has in mind this closed (non-recursive) form version of the function gfp(X) when writing the recursive definition. Proof that recursive definition R realizes gfp(X) requires showing that when each parameter appearing on the left of an equality is substituted for its appearance on the right equality holds under the condition associated with that equality. Proof of termination is also required. In a tail recursive function definition g(X) the form of non-terminal lines is g(X) = g(h(X)), and terminal lines g(X) = t(X). h(X) and g(X) are each a set of functions, on the parameters X. So the line f(n) = f(n-1) + f(n-2):n> 1 (read “: ” as “if”) could not appear in a tail recursive definition. The tail recursive definition form is of interest because it can be evaluated by a simple while program, namely one whose body contains assignment and conditional statements. For example, the tail recursiv