Mills' Functional Method: Procedures

OVERVIEW


Non-Recursive Procedures

Use textual substitution, after perhaps some alteration of variable names.

Assume we have

  procedure P (var x)
  begin
    T
  endproc
where T is a statement sequence that does not contain recursive calls to P, then this holds for code that calls P:
  [ ... P(y) ... ] = [ ... T' ... ]

Here, y is a set of actual parameters passed for the formals in the definition of P, and T' is a the body of P transformed to prevent variable name conflicts, as follows:
  1. occurrances of elements of x (the formal parameters to P) in T (the body of P) are replaced by corresponding elements of y (the actual parameters in the call to P)
  2. systematic renaming of local variables the "clash" with existing variable names in the calling environment... change these to "fresh" names

For example, consider this:

   procedure P (var n)       program main
   begin a:integer           begin a:integer
     a := 3                    a := 8
     n := 5                    P(a)
   endproc                     write(a)
                             end
After blind substitution:
   program main
   begin a:integer
     a := 8
     -- P(a)
       begin a:integer
         a := 3
         a := 5
       endproc
     write(a)
   end
Output from this code is "8". It is clear that the output is supposed to be 5 (with normal Pascal-ish semantics for procedure call-by-reference). The problem happens because the local "a" clashes with the global "a".

After corrected substitution (we rename the local "a" to "P_a"):

   program main
   begin a:integer
     a := 8
     -- P(a)
       begin p_a:integer
         P_a := 3
         a := 5
       endproc
     write(a)
   end

Recursive Procedures

The problem: Given recursive procedure P, find [P].

Substitution won't work, since the substituting process would not terminate.

We will use a method similar to loops: take a "guess" at [P], and use a theorem to demonstrate the guess is good.




Notes