Format: PDF / Kindle (mobi) / ePub
This unique guide book explains and teaches the concept of trustworthy compilers based on 50+ years of worldwide experience in the area of compilers, and on the author’s own 30+ years of expertise in development and teaching compilers. It covers the key topics related to compiler development as well as compiling methods not thoroughly covered in other books. The book also reveals many state-of-the-art compiler development tools and personal experience of their use in research projects by the author and his team. Software engineers of commercial companies and undergraduate/graduate students will benefit from this guide.
SUPER-attributed compiler compiler developed in the 1970s in the Computing Center of Russian Academy of Sciences, Moscow. The project was supervised by Dr. Vladimir M. Kurochkin. A really amazing compiler project in the 1970s was developed at our St. Petersburg University—implementation of ALGOL-68 for Soviet clones of IBM 360 . The project was lead by Dr. Gregory S. Tseytin who gathered a team of about 20 best compiler experts from our university. Due to the enthusiasm of the developers, the
opinion, the main issue of this model, as well as of any other kind of logic-based program semantic models, is that it relies on the mathematical concept of a variable (as a denotation for an entity whose value is constant within some reasoning block), rather than on the quite different concept of a variable in programming—as a named cell whose value is changeable by special executable statements, which follows the ideas of von Neumann’s computer architecture model of the 1940s. So, any
complicated architecture, far from their everyday tasks. So, this approach looks suitable for veriﬁed compilers but doesn’t seem applicable for verifying compilers. Denotational semantics approach is based on nontrivial mathematical ideas and foundation principles. This approach considers a program to be a predicate transformer—a kind of higher-order function, or functional, speaking in mathematical terms. The classicists of denotational semantics are Scott, Strachey, and Donahue. Its main idea
to check the formal conditions to hold on the Spec# program, or produce a list of veriﬁcation error messages if any of the conditions are violated. The communication with the veriﬁer is performed by the user in interactive mode. If necessary, the user can modify either the speciﬁcation part or the implementation part of the Spec# source code, to meet the veriﬁcation conditions. We pay a lot of attention to Spec# and do consider this programming system as the ﬁrst commercial trustworthy compiler.
the LL(k) and LR(k) classes of languages. Let’s brieﬂy overview the theoretical issues related to the LL and LR classes of formal languages [5,49]. All the programming languages (except for ALGOL-68 as you hopefully remember) belong to these classes. Let LL(k) be the class of all languages whose syntax can be deﬁned by an LL(k) grammar for some k >= 1. Then, the problem to check if LL(k) = LL(1) for some k is undecidable. Practically, it means that, if there is an LL(k) grammar for some k > 1