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

Refinement of Recursive Procedures with Parameters in PVS

Viorel Preoteasa, Refinement of Recursive Procedures with Parameters in PVS. TUCS Technical Reports 596, Turku Centre for Computer Science, 2004.

Abstract:

We present a shallow embedding in PVS of a predicate transformer semantics of an imperative language suitable for reasoning about
recursive procedures with parameters and local variables. We use
the PVS dependent type mechanism for implementing program variables
of different types. We use an uninterpreted state space and define
the program variables behavior by means of certain tree functions
that are supposed to satisfy some axioms. Unlike in the implementations
mentioned in the literature, we do not need to change the state space
when adding local variables or procedure parameters.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tPreoteasa04a,
  title = {Refinement of Recursive Procedures with Parameters in PVS},
  author = {Preoteasa, Viorel},
  number = {596},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2004},
  ISBN = {952-12-1319-1},
}

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

Edit publication