Зарегистрироваться
Восстановить пароль
FAQ по входу

Müller-Olm M. Modular Compiler Verification. A Refinement-Algebraic Approach Advocating Stepwise Abstraction

  • Файл формата pdf
  • размером 4,45 МБ
  • Добавлен пользователем
  • Отредактирован
Müller-Olm M. Modular Compiler Verification. A Refinement-Algebraic Approach Advocating Stepwise Abstraction
Издательство Springer, 1997, -256 pp.
After 40 years of practice and theory in compiler construction and 30 years of experience and teaching in software engineering we still observe that safety-critical high-level language programs are certified only together with the corresponding machine code. The reason is that certification institutions do not trust any compiler. And they are quite right: whereas errors detected in processor hardware are generally perceived as sensations, errors in software, even in system software, are commonplace.
It is high time to reverse this trend. Computer scientists should concentrate their abilities, experiences, and insights on the safe mastery of realistic system software. This particularly concerns realistic compilers for realistic programming languages running on hardware processors, as correct compilers play a central role in the construction of trustworthy application and system programs. Both application programmers and system software engineers need trusted development environments that permit them to concentrate on software specification and high-level implementation instead of wasting their time again and again with compilation problems and machine code inspection.
In order to construct fully correct and realistic compilers useful for safety-critical applications one must master two problems: compiling specification verification and compiler implementation verification. The first problem is to specify and prove semantically correct a mathematical translation function from high-level source programs to realistic target machine code. The second problem is to correctly refine and implement such a function either in a host language for which there is a running and trusted host compiler or in the machine language of a real host processor. Clearly, initially only the second way is trustworthy. M. Müller-Olm lays foundations for both problems.
One of the most characteristic aspects of M. Müller-Olm's way of thinking is his special way of looking at the behavior of hardware processors. He derives successively more elegant views, which allow real processors to be treated as idealized machines with ideal properties. This enables compiling verification techniques to be applied that rely on such machines. Future further propagation of the hierarchy of views promises clearer insights and proofs for the translation of even more ambitious realistic programming languages.
Introduction
Complete Boolean Lattices
Galois Connections
States, Valuation Functions and Predicates
The Algebra of Commands
Communication and
Data Refinement
Transputer Base Model
A Small Hard Real-Time Programming Language
A Hierarchy of Views
Compiling-Correctness Relations
Translation Theorems
A Functional Implementation
Conclusion
  • Чтобы скачать этот файл зарегистрируйтесь и/или войдите на сайт используя форму сверху.
  • Регистрация