Reasoning about recursive procedures with parameters

In this paper we extend the model of program variables from the Refinement Calculus [2] in order to be able to reason more algebraically about recursive procedures with parameters and local variables. We extend the meaning of variable substitution or freeness from the syntax to the semantics of program expressions. We give a predicate transformer semantics to recursive procedures with parameters and prove a

• Type: Conference
• Year: 2003
• Where: ICFP
• Authors: Ralph-Johan Back, Viorel Preoteasa
• Keywords: ICFP 2003, Predicate Transformer Semantics, Program Variables, Programming Languages, Recursive Procedures