Proving refinement transformations using extended denotational semantics Page: 1 of 18
This article is part of the collection entitled: Office of Scientific & Technical Information Technical Reports and was provided to UNT Digital Library by the UNT Libraries Government Documents Department.
Extracted Text
The following text was automatically extracted from the image on this page using optical character recognition software:
Proving Refinement Transformations Using
Extended Denotational Semantics "
OSTI
Victor L. Winter*
Intelligent Systems and Robotics Center
Sandia National Laboratories
Dept 9622. P.O. Box 5800
Albuquerque, NM 87185-0660, U.S.A.
vlwinte@sandia.gov
James M. Boylet
Mathematics and Computer Science Division
Argonne National Laboratory
Argonne, IL 60439, U.S.A.
boyle@mcs.anl.gov
Abstract
TAMPR is a fully automatic transformation system based on syn-
tactic rewrites. Our approach in a correctness proof is to map the
transformation into an axiomatized mathematical domain where for-
mal (and automated) reasoning can be performed. This mapping is
accomplished via an extended denotational semantic paradigm.
In this approach, the abstract notion of a program state is dis-
tributed between an environment function and a store function. Such
a distribution introduces properties that go beyond the abstract state
that is being modeled. The reasoning framework needs to be aware of
these properties in order to successfuly complete a correctness proof.
This paper discusses some of our experiences in proving the cor-
rectness of TAMPR transformations.
*This work was supported by the United States Department of Energy under Contract
DE-AC04-94AL85000.
tThis work was supported in part by the Mathematical, Information, and Computa-
tional Sciences Division subprogram of the Office of Computational and Technology Re-
search, U.S. Department of Energy, under Contract W-31-109-Eng-38, and in part by the
BM/C3 directorate, Ballistic Missle Defense Organization, U.S. Department of Defense.
1
DISTRUTON OF THIS DOOUtENT iS I -M) MAI E
Upcoming Pages
Here’s what’s next.
Search Inside
This article can be searched. Note: Results may vary based on the legibility of text within the document.
Tools / Downloads
Get a copy of this page or view the extracted text.
Citing and Sharing
Basic information for referencing this web page. We also provide extended guidance on usage rights, references, copying or embedding.
Reference the current page of this Article.
Winter, V.L. & Boyle, J.M. Proving refinement transformations using extended denotational semantics, article, April 1, 1996; Albuquerque, New Mexico. (https://digital.library.unt.edu/ark:/67531/metadc666738/m1/1/: accessed April 19, 2024), University of North Texas Libraries, UNT Digital Library, https://digital.library.unt.edu; crediting UNT Libraries Government Documents Department.