@inproceedings{
    inpBaPr03a,
    author = "Back, Ralph-Johan and Preoteasa, Viorel",
    publisher = "{ACM} Press",
    title = "Reasoning about Recursive Procedures with Parameters",
    booktitle = "Proceedings of the 2003 Workshop on Mechanized Reasoning about Languages with Variable Binding",
    year = "2003",
    lab = "Software Construction",
    month = "Aug",
    project = "refinement",
    flags = "copy",
    address = "New York, {NY}, {USA}",
    keywords = "Refinement Calculus, Recursive procedures",
    pdf = "inpBaPr03a.pdf",
    abstract = "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 refinement rule for introduction of recursive procedure calls. We also prove a Hoare total correctness rule for our recursive procedures. These rules have no side conditions and are easier to apply to programs than the ones in the literature. The theory is built having in mind mechanical verification support using theorem provers like PVS [18] or HOL [11]."
}