Concepts of Programming Languages PDF

Concepts of Programming Languages Dr. Mohammed A. Awadallah First semester 2022/2023 Chapter 3 Describing Syntax and Semantics ISBN 0-321-49362-1 Chapter 3 Topics Introduction The General Problem of Describing Syntax Formal Methods of D...

Concepts of Programming Languages Dr. Mohammed A. Awadallah First semester 2022/2023 Chapter 3 Describing Syntax and Semantics ISBN 0-321-49362-1 Chapter 3 Topics Introduction The General Problem of Describing Syntax Formal Methods of Describing Syntax Attribute Grammars Describing the Meanings of Programs: Dynamic Semantics Copyright © 2015 Pearson. All rights reserved. 1-3 Introduction One of the problems in describing a language is the diversity of the people who must understand the description: – Initial evaluators, people within the organization that employs the language’s designer, before their designs are completed. – Implementors obviously must be able to determine how the expressions, statements, and program units of a language are formed, and also their intended effect when executed. – Programmers/User must be able to determine how to encode software solutions by referring to a language reference manual. Textbooks and courses enter into this process. Copyright © 2015 Pearson. All rights reserved. 1-4 Introduction The study of programming languages, like the study of natural languages, can be divided into examinations of syntax and semantics. – Syntax: the form or structure of the expressions, statements, and program units. e.g. while (boolean_expr) statement (Java code) – Semantics: the meaning of the expressions, statements, and program units. The meaning of while (boolean_expr) statement If the Boolean expression is true, the embedded statement is executed. Then control implicitly returns to the Boolean expression to repeat the process. If the Boolean expression is false, control transfers to the statement following the while construct. Copyright © 2015 Pearson. All rights reserved. 1-5 The General Problem of Describing Syntax: Terminology A language, whether natural (such as English) or artificial (such as Java),is a set of sentences/statements A sentence is a string of characters over some alphabet A lexeme is the lowest level syntactic unit of a language (e.g., *, sum, begin). – The lexemes of a programming language include its numeric literals, operators, and special words, among others Copyright © 2015 Pearson. All rights reserved. 1-6 The General Problem of Describing Syntax: Terminology A token is a category of lexemes (e.g., identifier) e.g. index = 2 * count + 17; Lexemes Tokens index identifier = equal_sign 2 int_literal * mult_op count identifier + plus_op 17 int_literal ; semicolon Copyright © 2015 Pearson. All rights reserved. 1-7 Formal Definition of Languages In general, languages can be formally defined in two distinct ways: by recognition and by generation Recognizers – A recognition device reads input strings over the alphabet of the language and decides whether the input strings belong to the language – Example: syntax analysis part of a compiler - Detailed discussion of syntax analysis appears in Chapter 4 Generators – A device that generates sentences of a language – One can determine if the syntax of a particular sentence is syntactically correct by comparing it to the structure of the generator Copyright © 2015 Pearson. All rights reserved. 1-8 Formal Methods of Describing Syntax Context-Free Grammars – Developed by Noam Chomsky in the mid-1950s – Language generators, meant to describe the syntax of natural languages – Define a class of languages called context-free languages Backus-Naur Form (1959) – Invented by John Backus to describe the syntax of Algol 58 – BNF is equivalent to context-free grammars Copyright © 2015 Pearson. All rights reserved. 1-9 BNF Fundamentals A metalanguage is a language that is used to describe another language. BNF is a metalanguage for programming languages. In BNF, abstractions are used to represent classes of syntactic structures- – A simple Java assignment statement, for example, might be represented by the abstraction The abstraction in BNF can be terminals or non terminals Terminals are lexemes or tokens Copyright © 2015 Pearson. All rights reserved. 1-10 BNF Fundamentals A simple Java assignment statement, for example, might be represented by the abstraction The actual definition of can be given by = left-hand side (LHS) Right-hand side (RHS) nonterminal Terminal and/or nonterminal abstraction mixture of tokens, lexemes, and references to other abstractions Copyright © 2015 Pearson. All rights reserved. 1-11 BNF Fundamentals Nonterminals are often enclosed in angle brackets – Examples of BNF rules: → identifier | identifier, → if then Grammar: a finite non-empty set of rules A start symbol is a special element of the nonterminals of a grammar Copyright © 2015 Pearson. All rights reserved. 1-12 BNF Fundamentals Nonterminal symbols can have two or more distinct definitions, representing two or more possible syntactic forms in the language. (two or more RHS) Multiple definitions can be written as a single rule, with the different definitions separated by the symbol |, meaning logical OR. Copyright © 2015 Pearson. All rights reserved. 1-13  Describing Lists Variable-length lists in mathematics are often written using an ellipsis (...); 1, 2,... is an example Syntactic lists are described using recursion A rule is recursive if its LHS appears in its RHS. → ident | ident, Copyright © 2015 Pearson. All rights reserved. 1-14  Grammars and Derivations A grammar is a generative device for defining languages. A derivation is a repeated application of rules, starting with the start symbol and ending with a sentence (all terminal symbols) Copyright © 2015 Pearson. All rights reserved. 1-15 An Example Grammar (1) → begin end → | ; → = → A | B | C → + | – | begin end => begin ; end => begin = ; end => begin A = ; end => begin A = + ; end => begin A = B + ; end => begin A = B + C ; end => begin A = B + ; end => begin A = B + C ; = end => begin A = B + C ; B = end => begin A = B + C ; B = end => begin A = B + C ; B = C end Copyright © 2015 Pearson. All rights reserved. 1-17 Derivations Every string of symbols in a derivation is a sentential form A sentence is a sentential form that has only terminal symbols A leftmost derivation is one in which the leftmost nonterminal in each sentential form is the one that is expanded A derivation may be neither leftmost nor rightmost Copyright © 2015 Pearson. All rights reserved. 1-18 An Example Grammar (2) → = → A| B | C → + | * | ( ) | Copyright © 2015 Pearson. All rights reserved. 1-19  An Example Derivation (2) By using leftmost derivation: Derivate “A = B * ( A + C )” => = => A = => A = * => A = B * => A = B * ( ) => A = B * ( + ) => A = B * ( A + ) => A = B * ( A + ) => A = B * ( A + C ) Copyright © 2015 Pearson. All rights reserved. 1-20 Parse Tree A hierarchical representation of a derivation A parse tree for the simple statement A = B * (A + C) Grammar 1-21 Copyright © 2015 Pearson. All rights reserved. Parse Tree Every internal node of a parse tree is labeled with a nonterminal symbol Every leaf is labeled with a terminal symbol. Every subtree of a parse tree describes one instance of an abstraction in the sentence. Copyright © 2015 Pearson. All rights reserved. 1-22 Ambiguity in Grammars A grammar is ambiguous if and only if it generates a sentential form that has two or more distinct parse trees – Example of ambiguity grammar for Simple Assignment Statements Copyright © 2015 Pearson. All rights reserved. 1-23 Ambiguity in Grammars A=B+C*A Copyright © 2015 Pearson. All rights reserved. 1-24 Ambiguity in Grammars → | const → / | - const - const / const const - const / const Copyright © 2015 Pearson. All rights reserved. const - const / const 1-25 Ambiguity in Grammars A grammar is ambiguous in two cases: – if the grammar generates a sentence with more than one leftmost derivation – if the grammar generates a sentence with more than one rightmost derivation. The compiler chooses the code to be generated for a statement by examining its parse tree. If a language structure has more than one parse tree, then the meaning of the structure cannot be determined uniquely. In many cases, an ambiguous grammar can be rewritten to be unambiguous but still generate the desired language. Copyright © 2015 Pearson. All rights reserved. 1-26 An Unambiguous Expression Grammar If we use the parse tree to indicate precedence levels of the operators, we cannot have ambiguity For example, x + y * z – This expression is it add and then multiply, or vice versa? – if * has been assigned higher precedence than + (by the language designer), multiplication will be done first, regardless of the order of appearance of the two operators in the expression. Copyright © 2015 Pearson. All rights reserved. 1-27 An Unambiguous Expression Grammar Example: An Unambiguous Grammar for Expressions → = → A | B | C → + | → * | → ( ) | Copyright © 2015 Pearson. All rights reserved. 1-28 An Unambiguous Expression Grammar - Leftmost derivation (A = B + C * A) => = => A = => A = + => A = + => A = + => A = + => A = B + => A = B + * => A = B + * => A = B + * => A = B + C * => A = B + C * => A = B + C * A Copyright © 2015 Pearson. All rights reserved. 1-29 An Unambiguous Expression Grammar - Rightmost derivation (A = B + C * A) => = => = + => = + * => = + * => = + * A => = + * A => = + * A => = + C * A => = + C * A => = + C * A => = + C * A => = B + C * A => A = B + C * A Copyright © 2015 Pearson. All rights reserved. 1-30 An Unambiguous Expression Grammar The unique parse tree for A = B + C * A using an unambiguous grammar Copyright © 2015 Pearson. All rights reserved. 1-31 Associativity of Operators When an expression includes two operators that have the same precedence (as * and / usually have) For example, A / B * C A semantic rule is required to specify which should have precedence. This rule is named associativity Example: A = A + B + C (A + B) + C = A + (B + C) Copyright © 2015 Pearson. All rights reserved. 1-32 Associativity of Operators Operator associativity can also be indicated by a grammar -> + | const (ambiguous) -> + const | const (unambiguous) + expr + expr + expr const const + expr const const const const Copyright © 2015 Pearson. All rights reserved. ambiguous 1-33 Associativity of Operators -> + const | const (unambiguous) unambiguous + const + const const Copyright © 2015 Pearson. All rights reserved. 1-34  Associativity of Operators A parse tree for A = B + C + A illustrating the associativity of addition → = → A | B | C → + | → * | → ( ) | Copyright © 2015 Pearson. All rights reserved. 1-35  Unambiguous Grammar for Selector Java if-then-else grammar -> if () | if () else If we also have → , this grammar is ambiguous. The ambiguity in garamer is illustrated as follows: if () if () else Copyright © 2015 Pearson. All rights reserved. 1-36 Unambiguous Grammar for Selector if (done == true) if (denom == 0) quotient = 0; else quotient = num / denom; First tree Copyright © 2015 Pearson. All rights reserved. 1-37 Unambiguous Grammar for Selector Second tree Copyright © 2015 Pearson. All rights reserved. 1-38 Unambiguous Grammar for Selector An unambiguous grammar for if-then-else -> | -> if () | a non-if statement -> if () | if () else There is just one possible parse tree, using this grammar, for the following sentential form: if () if () else Copyright © 2015 Pearson. All rights reserved. 1-39 Extended BNF Optional parts are placed in brackets [ ] -> ident [()] Alternative parts of RHSs are placed inside parentheses and separated via vertical bars → (+|-) const Repetitions (0 or more) are placed inside braces { } → letter {letter|digit} Copyright © 2015 Pearson. All rights reserved. 1-40 BNF and EBNF BNF → if () |if () else EBNF → if () [else ] Copyright © 2015 Pearson. All rights reserved. 1-41 BNF and EBNF BNF → + | - | → * | / | EBNF → {(+ | -) } → {(* | /) } Copyright © 2015 Pearson. All rights reserved. 1-42 Recent Variations in EBNF Alternative RHSs are put on separate lines Use of a colon (:) instead of => Use of opt for optional parts Use of oneof for choices – AssignmentOperator → one of = *= /= %= += -= = &= ^= |= Copyright © 2015 Pearson. All rights reserved. 1-43 Static Semantics There are some characteristics of programming languages that are difficult to describe with BNF, and some that are impossible. (Nothing to do with meaning). In Java, for example, a floating-point value cannot be assigned to an integer type variable, although the opposite is legal. This restriction can be specified in BNF, it requires additional nonterminal symbols and rules. Then the grammar become too large to be useful Copyright © 2015 Pearson. All rights reserved. 1-44 Static Semantics The static semantics of a language is only indirectly related to the meaning of programs during execution; rather, it has to do with the legal forms of programs (syntax rather than semantics). Static semantics is so named because the analysis required to check these specifications can be done at compile time. Copyright © 2015 Pearson. All rights reserved. 1-45 Static Semantics Categories of constructs that are trouble: - Context-free, but cumbersome (e.g., types of operands in expressions) - Non-context-free (e.g., variables must be declared before they are used) Copyright © 2015 Pearson. All rights reserved. 1-46 Attribute Grammars Attribute grammars (AGs) are a formal approach both to describing and checking the correctness of the static semantics rules of a program. Attribute grammars (AGs) have additions to CFGs to carry some semantic info on parse tree nodes Primary value of AGs: – Static semantics specification – Compiler design (static semantics checking) Copyright © 2015 Pearson. All rights reserved. 1-47 Attribute Grammars : Definition Def: An attribute grammar is a context-free grammar with the following additions: – For each grammar symbol x there is a set A(x) of attribute values – The set A(X) consists of two disjoint sets S(X) and I(X), called synthesized and inherited attributes, respectively. – Synthesized attributes are used to pass semantic information up a parse tree – Inherited attributes are used to pass semantic information down and across a tree. Copyright © 2015 Pearson. All rights reserved. 1-48 Attribute Grammars : Definition – Each rule has a set of functions that define certain attributes of the nonterminals in the rule – Each rule has a (possibly empty) set of predicates to check for attribute consistency Copyright © 2015 Pearson. All rights reserved. 1-49 Attribute Grammars: Definition Let X0 → X1... Xn be a rule Functions of the form S(X0) = f(A(X1),... , A(Xn)) define synthesized attributes Functions of the form I(Xj) = f(A(X0),... , A(Xn)), for 1 + | A | B | C actual_type: synthesized for and – It is used to store the actual type, int or real, of a variable or expression expected_type: inherited for – It is used to store the type, either int or real, that is expected for the expression, as determined by the type of the variable on the left side of the assignment statement Copyright © 2015 Pearson. All rights reserved. 1-52 Attribute Grammars (continued) How are attribute values computed? – If all attributes were inherited, the tree could be decorated in top-down order. – If all attributes were synthesized, the tree could be decorated in bottom-up order. – In many cases, both kinds of attributes are used, and it is some combination of top-down and bottom-up that must be used. Copyright © 2015 Pearson. All rights reserved. 1-53 Attribute Grammars of Simple Assignment Statements Copyright © 2015 Pearson. All rights reserved. 1-54  Attribute Grammars (continued) The following is an evaluation of the attributes, in an order in which it is possible to compute them: A = A + B 1-.actual_type  lookup (A)(Rule 4) 2-.expected_type .actual_type (Rule 1) 3-.actual_type  lookup (A)(Rule 4).actual_type  lookup (B)(Rule 4) 4-.actual_type  either int or real (Rule 2) 5-.actual_type ==.expected_type TRUE or FALSE (Rule 2) Copyright © 2015 Pearson. All rights reserved. 1-55 Attribute Grammars (continued) A parse tree for A = A + B Copyright © 2015 Pearson. All rights reserved. 1-56 Attribute Grammars (continued) The flow of attributes in the tree Copyright © 2015 Pearson. All rights reserved. 1-57 Attribute Grammars (continued) A fully attributed parse tree Copyright © 2015 Pearson. All rights reserved. 1-58 Semantics We now turn to the difficult task of describing the dynamic semantics, or meaning, of the expressions, statements, and program units of a programming language. Because of the power and naturalness of the available notation, describing syntax is a relatively simple matter. There is no single widely acceptable notation or formalism for describing dynamic semantics Copyright © 2015 Pearson. All rights reserved. 1-59 Semantics (continued) Several needs for a methodology and notation for semantics: – Programmers need to know what statements mean before they can use them in their programs. – Compiler writers must know exactly what language constructs do – Correctness proofs would be possible without testing – Compiler generators would be possible – Language designers could detect ambiguities and inconsistencies in their language. Copyright © 2015 Pearson. All rights reserved. 1-60 Operational Semantics Describe the meaning of a statement or program by specifying the effects of running it on a machine. Copyright © 2015 Pearson. All rights reserved. 1-61 Operational Semantics (continued) The effects on the machine (memory, registers, etc.) are viewed as the sequence of changes in its state, where the machine’s state is the collection of the values in its storage. Most programmer, written a small test program to determine the meaning of some programming language construct, often while learning the language machine languages are not used for formal operational semantics To use operational semantics for a high-level language, a virtual machine is needed Copyright © 2015 Pearson. All rights reserved. 1-62 Operational Semantics (continued) A hardware pure interpreter would be too expensive A software pure interpreter also has problems – The detailed characteristics of the particular computer would make actions difficult to understand – Such a semantic definition would be machine- dependent Copyright © 2015 Pearson. All rights reserved. 1-63 Operational Semantics (continued) A better alternative: A complete computer simulation The process: – Build a translator (translates source code to the machine code of an idealized computer) – Build a simulator for the idealized computer Evaluation of operational semantics: – Good if used informally (language manuals, etc.) – Extremely complex if used formally (e.g., Vienna – Definition Language (VDL)), it was used for describing semantics of PL/I. Copyright © 2015 Pearson. All rights reserved. 1-64 Operational Semantics (continued) Uses of operational semantics: – Language manuals and textbooks – Teaching programming languages Two different levels of uses of operational semantics: - Natural operational semantics: The highest level, interest with the final results of the execution - Structural operational semantics: The lowest level, used to determine the precise meaning of a program through an examination Evaluation - Good if used informally (language manuals, etc.) - Extremely complex if used formally (e.g.,VDL) Copyright © 2015 Pearson. All rights reserved. 1-65 Denotational Semantics Based on recursive function theory The most abstract semantics description method Originally developed by Scott and Strachey (1970) Copyright © 2015 Pearson. All rights reserved. 1-66 Denotational Semantics - continued The process of building a denotational specification for a language: - Define a mathematical object for each language entity – Define a function that maps instances of the language entities onto instances of the corresponding mathematical objects However, unlike operational semantics, denotational semantics does not model the step-by-step computational processing of programs. Copyright © 2015 Pearson. All rights reserved. 1-67 Denotational Semantics –Example 1 The syntax of such binary numbers can be described by the following grammar rules: → '0‘ | '1‘ | '0‘ | '1' A parse tree of the binary number 110 Copyright © 2015 Pearson. All rights reserved. 1-68 Denotational Semantics –Example 1 The semantic function, named Mbin, maps the syntactic objects to the objects in N, The semantic domain is the set of nonnegative decimal numbers, symbolized by N. Mbin('0') = 0 Mbin('1') = 1 Mbin( '0') = 2 * Mbin() Mbin( '1') = 2 * Mbin() + 1 Copyright © 2015 Pearson. All rights reserved. 1-69 Denotational Semantics –Example 1 This is syntax-directed semantics. Syntactic entities are mapped to mathematical objects with concrete meaning. A parse tree with denoted objects for 110 Copyright © 2015 Pearson. All rights reserved. 1-70 Decimal Numbers – Example 2 → '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | ('0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9') Mdec('0') = 0, Mdec ('1') = 1, …, Mdec ('9') = 9 Mdec ( '0') = 10 * Mdec () Mdec ( '1’) = 10 * Mdec () + 1 … Mdec ( '9') = 10 * Mdec () + 9 Copyright © 2015 Pearson. All rights reserved. 1-71 Denotational Semantics: program state The state of a program is the values of all its current variables s = {, , …, } Each i is the name of a variable, and the associated v’s are the current values of those variables. Any of the v’s can have the special value undef, which indicates that its associated variable is currently undefined. Copyright © 2015 Pearson. All rights reserved. 1-72 Denotational Semantics: program state Let VARMAP be a function that, when given a variable name and a state, returns the current value of the variable VARMAP(ij, s) = vj Copyright © 2015 Pearson. All rights reserved. 1-73 Expressions Expressions are fundamental to most programming languages We assume expressions are decimal numbers, variables, or binary expressions having one arithmetic operator and two operands, each of which can be an expression. → | | → → | → | → + | * Copyright © 2015 Pearson. All rights reserved. 1-74 Expressions - continued The only error we consider in expressions is a variable having an undefined value Let Z be the set of integers, and let error be the error value. Then Z  {error} is the semantic domain for the denotational specification for our expressions. The mapping function for a given expression E and state s follows Note that we use the symbol Δ = to define mathematical function Copyright © 2015 Pearson. All rights reserved. 1-75 Expressions - continued Me(, s) = case of => Mdec(, s) => if VARMAP(, s) == undef then error else VARMAP(, s) => if (Me(., s) == undef OR Me(., s) = undef) then error else if (. == '+' then Me(., s) + Me(., s) else Me(., s) * Me(., s)... Copyright © 2015 Pearson. All rights reserved. 1-76 Evaluation of Denotational Semantics Can be used to prove the correctness of programs Provides a rigorous way to think about programs Can be an aid to language design Has been used in compiler generation systems Because of its complexity, it are of little use to language users Copyright © 2015 Pearson. All rights reserved. 1-77 Axiomatic Semantics Based on mathematical logic (predicate calculus) axiomatic semantics specifies what can be proven about the program Original purpose: formal program verification Axioms or inference rules are defined for each statement type in the language (to allow transformations of logic expressions into more formal logic expressions) The logical expressions are called predicates, or assertions Copyright © 2015 Pearson. All rights reserved. 1-78 Axiomatic Semantics (continued) An assertion before a statement (a precondition) states the relationships and constraints among variables that are true at that point in execution An assertion following a statement is a postcondition A weakest precondition is the least restrictive precondition that will guarantee the validity of the associated postcondition Copyright © 2015 Pearson. All rights reserved. 1-79 Axiomatic Semantics Form Pre-, post form: {P} statement {Q} An example –a = b + 1 {a > 1} – {b > 10}, {b > 100}, {b > 500} are all valid preconditions – Weakest precondition: {b > 0} Copyright © 2015 Pearson. All rights reserved. 1-80  Program Proof Process A program proof is begun by using the characteristics of the results of the program’s execution as the postcondition of the last statement of the program. This postcondition, along with the last statement, is used to compute the weakest precondition for the last statement. This precondition is then used as the postcondition for the second last statement. Copyright © 2015 Pearson. All rights reserved. 1-81  Program Proof Process This process continues until the beginning of the program is reached. At that point, the precondition of the first statement states the conditions under which the program will compute the desired results. If these conditions are implied by the input specification of the program, the program has been verified to be correct. Copyright © 2015 Pearson. All rights reserved. 1-82 Axiomatic Semantics: Assignment Let x = E be a general assignment statement and Q be its postcondition. Then, its weakest precondition, P, is defined by the axiom P = Qx->E which means that P is computed as Q with all instances of x replaced by E. Example of assignment statment: – a = b / 2 - 1 {a < 10} – Postcondition is {a < 10} – The weakest precondition is b / 2 - 1 < 10 Copyright © 2015 Pearson. All rights reserved. b < 22 1-83 Axiomatic Semantics: Assignment Example#2 of assignment statment: x = 2 * y - 3 {x > 25} – Postcondition is {x > 25} – The weakest precondition is 2 * y - 3 > 25 y > 14 Example#3 of assignment statment: x = x + y - 3 {x > 10} – Postcondition is {x > 10} – The weakest precondition is x + y - 3 > 10 y > 13 - x Copyright © 2015 Pearson. All rights reserved. 1-84 Axiomatic Semantics: Rule of Consequence For example, consider the following logical statement: {x > 3} x = x - 3 {x > 0} Therefore, we need to prove the following logical statement. {x > 5} x = x - 3 {x > 0} The Rule of Consequence: {P}S {Q}, P'  P, Q  Q' {P'} S {Q'} Then, P is {x>3}, P’ is {x>5}, and Q, Q’ are {x>0} Copyright © 2015 Pearson. All rights reserved. 1-85 Axiomatic Semantics: Rule of Consequence The Rule of Consequence: {P}S {Q}, P'  P, Q  Q' {P'} S {Q'} The rule of consequence says that a postcondition can always be weakened and a precondition can always be strengthened The first term of the antecedent ({x > 3} x = x – 3 {x > 0}) was proven with the assignment axiom. The second and third terms are obvious. Therefore, by the rule of consequence, the consequent is true. Copyright © 2015 Pearson. All rights reserved. 1-86 Axiomatic Semantics: Sequences An inference rule for sequences of the form S1; S2 {P1} S1 {P2} {P2} S2 {P3} {P1}S1 {P2},{P2}S2 {P3} {P1}S1; S2 {P3} Copyright © 2015 Pearson. All rights reserved. 1-87 Axiomatic Semantics: Sequences For example, consider the following sequence and postcondition: y = 3 * x + 1; x = y + 3; {x < 10} The precondition for the second assignment statement is {y < 7} The precondition for the first assignment statement is 3*x+1 0}. y = y - 1 {y > 0} This produces {y - 1 > 0} or {y > 1}. It can be used as the P part of the precondition for the then clause. Copyright © 2015 Pearson. All rights reserved. 1-90 Axiomatic Semantics: Selection y = y + 1 {y > 0} This produces {y + 1 > 0} or {y > -1}. It can be used as the P part of the precondition for the else clause. Because {y > 1} => {y > -1}, the rule of consequence allows us to use {y > 1} for the precondition of the whole selection statement. Copyright © 2015 Pearson. All rights reserved. 1-91 Axiomatic Semantics: Loops An inference rule for logical pretest loops {P} while B do S end {Q} (I and B) S {I} {I} while B do S {I and (not B)} where I is the loop invariant (the inductive hypothesis) Copyright © 2015 Pearson. All rights reserved. 1-92 Axiomatic Semantics: Loops Characteristics of the loop invariant: I must meet the following conditions: – P => I -- the loop invariant must be true initially – {I} B {I} -- evaluation of the Boolean must not change the validity of I – {I and B} S {I} -- I is not changed by executing the body of the loop – (I and (not B)) => Q -- if I is true and B is false, Q is implied – The loop terminates -- can be difficult to prove Copyright © 2015 Pearson. All rights reserved. 1-93 Loop Invariant The loop invariant I is a weakened version of the loop postcondition, and it is also a precondition. I must be weak enough to be satisfied prior to the beginning of the loop, but when combined with the loop exit condition, it must be strong enough to force the truth of the postcondition Copyright © 2015 Pearson. All rights reserved. 1-94 Axiomatic Semantics: Loops For example, consider the following loop: while y x do y = y + 1 end {y = x} For zero iterations, the weakest precondition is, obviously, {y = x} For one iteration, it is wp(y = y + 1, {y = x}) = {y + 1 = x}, or {y = x - 1} For two iterations, it is wp(y = y + 1, {y = x - 1})={y + 1 = x - 1}, or {y = x - 2} For three iterations, it is wp(y = y + 1, {y = x - 2})={y + 1 = x - 2}, or {y = x – 3} Copyright © 2015 Pearson. All rights reserved. 1-95 Axiomatic Semantics: Loops It is now obvious that {y < x} will suffice for cases of one or more iterations. Combining {y 1 do s = s / 2 end {s = 1} Copyright © 2015 Pearson. All rights reserved. 1-98 Evaluation of Axiomatic Semantics Developing axioms or inference rules for all of the statements in a language is difficult It is a good tool for correctness proofs, and an excellent framework for reasoning about programs, but it is not as useful for language users and compiler writers Its usefulness in describing the meaning of a programming language is limited for language users or compiler writers Copyright © 2015 Pearson. All rights reserved. 1-99 Denotation Semantics vs Operational Semantics In operational semantics, the state changes are defined by coded algorithms In denotational semantics, the state changes are defined by rigorous mathematical functions Copyright © 2015 Pearson. All rights reserved. 1-100 Summary BNF and context-free grammars are equivalent meta-languages – Well-suited for describing the syntax of programming languages An attribute grammar is a descriptive formalism that can describe both the syntax and the semantics of a language Three primary methods of semantics description – Operation, axiomatic, denotational Copyright © 2015 Pearson. All rights reserved. 1-101