Advertisement

Verification

  • Andrew D. McGettrick
  • Owen Traynor
  • David Duffy
Part I: Methodology
  • 113 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 680)

Abstract

Verification is an important facet of the PROSPECTRA methodology. In this chapter general verification issues are considered as well as the conceptual and the practical integration of proof into the methodology. The proof systems available within the PROSPECTRA system are described and their complementary roles in program development are presented.

The way in which the PROSPECTRA methodology and system are used to construct proof strategies and tactics is described. The principles underlying proof are closely related to the methodology for transformation and program development, and indeed a certain duality is apparent. This duality is exposed and shown to underpin many aspects of the design of the proof system.

Keywords

Transformation Rule Proof System Sequent Calculus Transformational Programming Proof Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Andrew D. McGettrick
    • 1
  • Owen Traynor
    • 1
  • David Duffy
    • 1
  1. 1.University of StrathclydeGermany

Personalised recommendations