Semantics with Applications: An Appetizer (Undergraduate Topics in Computer Science)
Hanne Riis Nielson
Language: English
Pages: 274
ISBN: 1846286913
Format: PDF / Kindle (mobi) / ePub
Semantics will play an important role in the future development of software systems and domain-specific languages. This book provides a needed introductory presentation of the fundamental ideas behind these approaches, stresses their relationship by formulating and proving the relevant theorems, and illustrates the applications of semantics in computer science. Historically important application areas are presented together with some exciting potential applications. The text investigates the relationship between various methods and describes some of the main ideas used, illustrating these by means of interesting applications. The book provides a rigorous introduction to the main approaches to formal semantics of programming languages.
The rules [compsos we first execute S 1 one step from s. Then there are two possible outcomes: 34 2. Operational Semantics – If the execution of S 1 has not been completed, we have to complete it before embarking on the execution of S 2 . – If the execution of S 1 has been completed, we can start on the execution of S 2. 1 ]: if the result of executing the The first case is captured by the rule [compsos first step of ⟨S , s⟩ is an intermediate configuration ⟨S ′1 , s ′ ⟩, then the next
statement as an atomic entity that cannot be split into smaller pieces. This may be summarized as follows: Natural Semantics versus Structural Operational Semantics • In a natural semantics, the execution of the immediate constituents is an atomic entity so we cannot express interleaving of computations. • In a structural operational semantics, we concentrate on the small steps of the computation so we can easily express interleaving. Exercise 3.5 Consider an extension of While that in
result follows. tt The case [ifns ]: Assume that ⟨if b then S 1 else S 2 , s⟩ → s ′ because B[[b]]s = tt and From Table 4.3, we get that ⟨S 1 , s⟩ → s ′ CS[[if b then S 1 else S 2 ]] = CB[[b]]:branch(CS[[S 1 ]], CS[[S 2 ]]) Using Exercises 4.19 and 4.4 we get the first part of ⟨CB[[b]]:branch(CS[[S 1 ]], CS[[S 2 ]]), ε, s⟩ ◃∗ ⟨branch(CS[[S 1 ]], CS[[S 2 ]]), (B[[b]]s), s⟩ ◃ ⟨CS[[S 1 ]], ε, s⟩ ◃∗ ⟨ε, ε, s ′ ⟩ The second part follows from the definition of the meaning of the instruction
CA[[a]]:store-x so assume that ⟨CA[[a]]:store-x , ε, s⟩ ◃k0 +1 ⟨ε, e, s ′ ⟩ Then, by Exercise 4.5, there must be a configuration of the form ⟨ε, e ′′ , s ′′ ⟩ such that and ⟨CA[[a]], ε, s⟩ ◃k1 ⟨ε, e ′′ , s ′′ ⟩ ⟨store-x , e ′′ , s ′′ ⟩ ◃k2 ⟨ε, e, s ′ ⟩ where k1 + k2 = k0 + 1. From Lemma 4.18 and Exercise 4.6, we get that e ′′ must be (A[[a]]s) and s ′′ must be s. Using the semantics of store-x we therefore see that s ′ is s[x →A[[a]]s] and e is ε. It now follows from [assns ] that ⟨x :=a,
is a reference outside the bounds of array a”. Such information is the result of various program analyses. The first warning is the result of a definition-use analysis: at each point of a program where the value of a variable is used, the analysis will determine those points where the variable might have obtained its present value; if there are none, then clearly the variable is uninitialised. The second warning might be the result of a constant propagation analysis: at each point of a program