• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Reasoning About Recursive Procedures with Parameters

Ralph-Johan Back, Viorel Preoteasa, Reasoning About Recursive Procedures with Parameters. In: Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding, , ACM Press, New York, NY, USA, 2003.

Abstract:

In this paper we extend the model of program variables from the Refinement Calculus 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 or HOL.

Files:

Full publication in PDF-format

BibTeX entry:

@INPROCEEDINGS{inpBaPr03a,
  title = {Reasoning About Recursive Procedures with Parameters},
  booktitle = {Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding},
  author = {Back, Ralph-Johan and Preoteasa, Viorel},
  publisher = {ACM Press, New York, NY, USA},
  pages = { },
  year = {2003},
  keywords = {Refinement Calculus, Recursive procedures},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication