Changeset 512


Ignore:
Timestamp:
Feb 15, 2011, 10:39:42 AM (6 years ago)
Author:
mulligan
Message:

tidy up of the intro

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r511 r512  
    1010\usepackage[utf8x]{inputenc}
    1111\usepackage{listings}
     12\usepackage{mdwlist}
    1213\usepackage{microtype}
    1314\usepackage{stmaryrd}
     
    8182\label{sect.introduction}
    8283
    83 Formal methods are aimed at increasing our confidence in our software and
    84 hardware artifacts. Ideally, in the future we would like all artifacts to be
    85 equipped with a formal specification and a proof of correctness of the
    86 implementation. Nowadays practically all programs are written in high level
    87 languages and then compiled into low level ones. Thus the specifications are
    88 also given at high level and correctness is proved reasoning automatically
    89 or interactively on the source code. The code that is actually run, however,
    90 is the object code generated by the compiler.
    91 
    92 A few simple questions then arise:
     84Formal methods are designed to increase our confidence in the design and implementation of software (and hardware).
     85Ideally, we would like all software to come equipped with a formal specification, along with a proof of correctness for the implementation.
     86Today practically all programs are written in high level languages and then compiled into low level ones.
     87Specifications are therefore also given at a high level and correctness can be proved by reasoning automatically or interactively on the program's source code.
     88The code that is actually run, however, is not the high level source code that we reason on, but the object code that is generated by the compiler.
     89
     90A few simple questions now arise:
     91\begin{itemize*}
     92\item
    9393What properties are preserved during compilation?
     94\item
    9495What properties are affected by the compilation strategy?
     96\item
    9597To what extent can you trust your compiler in preserving those properties?
    96 
    97 Compiler verification, as of late, is a `hot topic' in computer science
    98 research. So far, it has been focused on the first and last question only.
    99 In particular, the attention has been put only on extensional properties,
    100 which are easily preserved during compilation:
    101 it is sufficient to completely preserve the denotational semantics of the
    102 input program.
     98\end{itemize*}
     99
     100These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification}.
     101So far, the field has been focused on the first and last questions only.
     102In particular, much attention has been placed on verifying compiler correctness with respect to extensional properties of programs, which are easily preserved during compilation; it is sufficient to completely preserve the denotational semantics of the input program.
    103103
    104104The situation is definitely more complex when we also take in account
Note: See TracChangeset for help on using the changeset viewer.