• 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. TUCS Technical Reports 500, Turku Centre for Computer Science, 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:

@TECHREPORT{tBaPr03a,
  title = {Reasoning about Recursive Procedures with Parameters},
  author = {Back, Ralph-Johan and Preoteasa, Viorel},
  number = {500},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2003},
  keywords = {Refinement, Recursive procedures, Semantics, Hoare rules},
  ISBN = {952-12-1104-0},
}

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

Edit publication