# Mills' Functional Method: Procedures

## 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.

### Theorem:

Given a procedure declared as:

```   procedure P ( var w )
begin
if b then S1; P(w); S2
else S3
endproc
```
where w is a list of parameters passed by reference, b is a boolean expression, and S1, S2, and S3 are statement sequences that DO NOT contain calls to P, then

f = [P] if and only if

1. dom(f) = dom([P])
2. f = ( [b] --> [S1] o f o [S2] ) | ( ~[b] --> [S3] )

### Notes

• You may have to rewrite a procedure P into some other procedure P' in order to apply this theorem, since it requires a particular form. If you have to rewrite, then you have a proof obligation (informal) to show that [P'] = [P].