By Susan Stepney
Illustrating a course for mathematically specifying and carefully imposing a excessive insurance compiler appropriate to be used in constructing excessive integrity purposes, this e-book explains some of the thoughts used at each one degree of the advance, and is illustrated all through via a compiler for a small significant language, focusing on a standard guideline set.
Read Online or Download High integrity compilation: a case study PDF
Similar compilers books
Initially released in 1981, this used to be the 1st textbook on programming within the Prolog language and remains to be the definitive introductory textual content on Prolog. although many Prolog textbooks were released due to the fact, this one has withstood the try out of time due to its comprehensiveness, instructional procedure, and emphasis on basic programming functions.
- Formal Methods for Industrial Critical Systems: 19th International Conference, FMICS 2014, Florence, Italy, September 11-12, 2014. Proceedings
- Algorithms for Parallel Polygon Rendering
- Constraint Solving and Language Processing: First International Workshop, CSLP 2004, Roskilde, Denmark, September 1-3, 2004, Revised Selected and
- Automatic SIMD Vectorization of SSA-based Control Flow Graphs
Extra resources for High integrity compilation: a case study
At rst sight, this technique may look more complicated than using plain Prolog. It does, however, have the advantage of cleanly separating the syntax and semantics. Another important advantage of this approach is that a DCTG can be used to support multiple sets of di erent semantics attached to each node, as extra elements in the node list. So Turandot's choice command can be written using 30 Chapter 3. Using Prolog the DCTG formalism, including the code template (compiler), dynamic semantics (interpreter), and static semantics (static checker), as command ::= tIF, expr^^E, tTHEN, command^^Cthen, tELSE, command^^Celse <:> (static(PreSState, PostSState) ::Cthen^^static(PreSState, SState1), Celse^^static(PreSState, SState2), intersection(SState1, SState2, PostSState) ), (dynamic(PreState, PostState) ::E^^dynamic(PreState, Value), ( Value = 1, Cthen^^dynamic(PreState, PostState) ; Value = 0, Celse^^dynamic(PreState, PostState) ) ), (compile( InstrExpr, jump(L1), InstrThen, goto(L2), label(L1), InstrElse, label(L2)] ) ::E^^compile(InstrExpr), Cthen^^compile(InstrThen), Celse^^compile(InstrElse) ).
This clause declares that, for a skip command, the PreState and PostState have the same value, whatever that value is. If the clause is being executed, as part of a Turandot interpreter, a value would be supplied for PreState, and PostState would become instantiated with the same value: command(assign(Name,Expr), PreState, PostState) :expr(Expr, PreState, Value), updatestate(Name, Value, PreState, PostState). This clause declares that, for an assign command, Value is the value of Expr in the PreState, and that the PreState updated with Name and Value is the PostState.
1 1 & 2 ) g dom & 2 & 1 fcheckWrong g dom & 1 & 2 fcheckWrong g is Z's range restriction: the relation S r is that subset of the relation S that has its range restricted to the elements in r . is Z's domain anti-restriction: the relation d S is that subset of the relation S that has its domain restricted to the elements not in d . For example, fa 7! 1; b 7! 2; c 7! 3g f1; 2g = fa 7! 1; b 7! 2g fa g fa 7! 1; b 7! 2; c 7! 3g = fb 7! 2; c 7! 3g fa g fa 7! 1; b 7! 2; c 7! 3g f1; 2g = fb 7! 2g The de nition of worseStore is one of the more complicated-looking de nitions, so, to see how it works, consider two stores: & 1 = f 1 7!