Procedures, parameters, and abstraction: Separate concerns

AbstractThe notions of procedures, parameters, and abstraction are by convention treated together in methods of imperative program development. Rules for preserving correctness in such developments can be complex.We show that the three concerns can be separated, and we give simple rules for each. Crucial to this is the ability to embed specification—representing abstraction—directly within programs; with this we can use the elegant copy rule of ALGOL-60 to treat procedure calls, whether abstract or not.Our contribution is in simplifying the use of the three features, whether separately or together, and in the proper location of any difficulties that do arise. The aliasing problem, for example, is identified as a “loss of monotonicity” with respect to program refinement