Entry Aiken:1995:SST from toplas.bib

Last update: Tue May 1 02:05:46 MDT 2012                Valid HTML 3.2!

Index sections

Top | Symbols | Math | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z

BibTeX entry

@Article{Aiken:1995:SST,
  author =       "Alexander Aiken and John H. Williams and Edward L.
                 Wimmers",
  title =        "Safe: {A} Semantic Technique for Transforming Programs
                 in the Presence of Errors",
  journal =      j-TOPLAS,
  volume =       "17",
  number =       "1",
  pages =        "63--84",
  month =        jan,
  year =         "1995",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925 (print), 1558-4593 (electronic)",
  ISSN-L =       "0164-0925",
  bibdate =      "Fri Jan 5 07:58:42 MST 1996",
  bibsource =    "http://www.math.utah.edu/pub/tex/bib/toplas.bib",
  URL =          "http://www.acm.org/pubs/toc/Abstracts/0164-0925/201002.html",
  abstract =     "Language designers and implementors have avoided
                 specifying and preserving the meaning of programs that
                 produce errors. This is apparently because being forced
                 to preserve error behavior limits severely the scope of
                 program optimization, even for correct programs.
                 However, error behavior preservation is desirable for
                 debugging, and error behavior must be preserved in any
                 language that permits user-generated errors (i.e.,
                 exceptions).\par

                 This article presents a technique for expressing
                 general program transformations for languages that
                 possess a rich collection of distinguishable error
                 values. This is accomplished by defining a higher-order
                 function called {\bf Safe}, which can be used to
                 annotate those portions of a program that are
                 guaranteed not to produce errors. It is shown that this
                 facilitates the expression of very general program
                 transformations, effectively giving program
                 transformations in a language with many error values
                 the same power and generality as program
                 transformations in a language with only a single error
                 value.\par

                 Using the semantic properties of {\bf Safe}, it is
                 possible to provide some useful sufficient conditions
                 for establishing the correctness of transformations in
                 the presence of errors. In particular, a
                 Substitutability theorem is proven, which can be used
                 to justify ``in-context'' optimizations:
                 transformations that alter the meanings of
                 subexpressions without changing the meaning of the
                 whole program. Finally, the effectiveness of the
                 technique is demonstrated by some examples of its use
                 in an optimizing compiler.",
  acknowledgement = ack-nhfb,
  fjournal =     "ACM Transactions on Programming Languages and
                 Systems",
  keywords =     "languages; theory",
  subject =      "{\bf D.3.4}: Software, PROGRAMMING LANGUAGES,
                 Processors, Optimization. {\bf D.3.1}: Software,
                 PROGRAMMING LANGUAGES, Formal Definitions and Theory,
                 Semantics.",
}

Related entries