Assume we have
procedure P (var x) begin T endprocwhere T is a statement sequence that does not contain recursive calls to P, then this holds for code that calls P:
[ ... P(y) ... ] = [ ... T' ... ]
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) endAfter blind substitution:
program main begin a:integer a := 8 -- P(a) begin a:integer a := 3 a := 5 endproc write(a) endOutput 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
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.
Given a procedure declared as:
procedure P ( var w ) begin if b then S1; P(w); S2 else S3 endprocwhere 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