Describing Syntax and Semantics

[jimin-kiim]

• Introduction
• the General Problem of Describing Syntax
• Formal Methods of Describing Syntax
• Static Semantics and Attribute Grammars
• Dynamic Semantics

[jimin-kiim]

Introduction

• Syntax : the form of structure of the expressions, statements and program units
• Semantics : the meaning of the expressions, statements and program units
• Syntax and Semantics provide a language's definition for users
  • users of a language definition
  • other language designers
  • implementers
  • programmers(the users of the language)

$Syntax$ : while(bool_expr) statement $Semantics$ : "when the current value of the Boolean expression is true, the embedded statement is executed. If the Boolean expression if false, control transfers to the statement following the while construct"

[jimin-kiim]

the General Problem of Describing Syntax

• language : a set of sentences
• sentence : a string of characters over some alphabet
• lexeme : the lowest level syntactic unit of a language
• token : a category of lexemes

sentence index = 2 * count + 17;

lexemes index, =, 2, *, count, +, 17, ;

tokens - lexemes identifier - index, count int_literal - 2, 17 equal_sign - = mult_op - * plus_op - + semicolon - ;

• language recognizers (syntax analyzer, parsers)
  • a recognition device reads input string over the alphabet of the language and decides whether the input strings belong to the language(syntax checking)
  • syntax analysis part of a compiler
• language 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

[jimin-kiim]

Formal Methods of Describing Syntax(1)

BNF(Backus-Naus Form)

• metalanguage for programming languages
  • metalanguage : a language that is used to describe another language.
• invented by John Backus to describe the syntax of Algol 58
• a formal notation for specifying programming language syntax
• equivalent to context free grammars
  • CFG(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

• terminals : lexemes and tokens
• abstractions(syntactic variables, nonterminal symbols or nonterminals)
  • used to represent classes of syntactic structures
  • references to other abstractions
  • enclosed in angle brackets
• LHS(Left Hand Side) : the left side of the arrow where the abstraction is defined
• RHS(Right Hand Side) : the right side of the arrow where the string of terminals and/or nonterminals is placed. An abstraction can have more than one RHS
• a rule is recursive if its LHS appears in its RHS.

• grammar : a collection of rules
• BNF grammar is a finite non-empty set of rules
• derivation : a sequence of rule applications, a repeated application of rules
  • derivation starts with the start symbol and end with a sentence consisting of terminal symbols only
  • start symbol : a special nonterminal of grammar where any sentences of a language begin
  • The sentences of a language are generated through derivation
  • sentential form : every string of symbols in a derivation
  • sentence : a sentential from that has only terminal symbols (end result of derivation)
  • a left[right]most derivation : expanding the left[right]most nonterminal in each sentential form
  • a derivation may be neither leftmost nor rightmost
  • parse tree : a hierarchical representation of a derivation

    
    Grammar

-> begin end -> | ; -> = -> a|b|c|d -> + | - -> | const ``` ``` Derivation a = b + const => begin end => begin end => begin = end => begin a = end => begin a = + end => begin a = b + end => begin a = b + const end ``` - ambiguity in grammar - grammar is ambiguous iff it generates a sentential form that has two or more distinct parse trees - if we use the parse tree to indicate precedence levels of the operators, there will be no ambiguity. The higher precedence operator should be lower in the parse tree - associativity of operators : when an expression includes two operators that have the same precedence, a semantic rule is required to specify which should have precedence. ``` Ambiguous -> if () then | if () then else ``` ``` Unambiguous -> | -> a non-if statement | if () then else -> if () then | if () then else There is just one possible parse tree, using this grammar, for the following sentential form; if () if () else ```

[jimin-kiim]

Formal Methods of Describing Syntax(2)

EBNF(Extended BNF)

• optional parts are placed in brackets [ ]
• repetitions are placed inside braces { }
• alternative parts of RHSs are placed inside parentheses and separated via vertical bars |

  
  <if_stmt> → if (<expression>) <statement> [else <statement>]

for

→ if () | if () else ``` ``` → {, } ``` ``` → (* | / | %) for → * | / | % ``` - recent variations in EBNF - a colon is used instead of the arrow - the RHS is placed on the next line - in the place of square brackets to indicate something being optional, the subscript 'opt' is used. - rather than using the | symbol in a parenthesized list of elements to indicate a choice, the word "oneof" are used.

[jimin-kiim]

Semantics

• meaning of the expressions, statements and program units of a programming language.

Static Semantics and Attribute Grammars

Static Semantics

• nothing to do with meaning
• CFGs(Context Free Grammars) cannot describe all of the syntax of programming languages.
  • Context-free but cumbersome constructs
  • In Java, for example, a floating point value cannot be assigned to an integer type variable, although the opposite is legal. If all of the typing rules of Java were specified in BNF, the grammar would become too large to be useful, since the size of the grammar determines the size of the syntax analyzer.
  • Non-context-free constructs
  • variables must be declared before they are used
• static semantics of a language is only indirectly related to the meaning of programs and states mostly about its type constraints
• the analysis required to check these specifications can be done at compile time, so it's named 'static semantics'

  Attribute Grammar(AG)

  • a device used to describe more of the structure of a programming language that can be described with a context free grammar.
  • a CFG to which have been added attributes, attribute computation functions and predicate functions.
  • attributes(attribute values) A(X) : are associated with grammar symbols. Each grammar symbol X is a set of attributes A(X). A(X) = S(X) ∪ I(X)
    • synthesized attributes S(X) : used to pass semantic information up a parse tree
    • inherited attributes I(X) : used to pass semantic information down and across a tree
    • intrinsic attributes : synthesized attributes of leaf nodes whose values are determined outside the parse tree.
  • attribute computation functions(semantic functions) : are associated with grammar rules and used to specify how attribute values are computed. Define certain attributes of the non-terminals in the rule.
  • predicate functions : are associated with grammar rules and state the static semantic rules of the language. Check for attribute consistency
  • CFG + Semantic rules

    
    Syntax 
    <assign> -> <var> = <expr>

Semantics

.expected_type <- .actual_type ``` ``` -> + | Syntax -> Semantics .actual_type <- .actual_type Syntax -> [1] + [2] Semantics .actual_type <- [1].actual_type predicate [1].actual_type == [2].actual_tye .expected_type == .actual_type ``` ``` Syntax -> A | B | C Semantics .actual_type <- look-up(.string) ``` actual_ type : a synthesized attribute related to \ and \ expected_type : an inherited attribute related to \ computing attributing values - 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's some combination of top-down and bottom-up that must be used.

[jimin-kiim]

Dynamic Semantics

Operational Semantics

• describe the meaning of a statement or program by specifying the effects of running it on a machine. The effects on the machine are viewed as the sequence of changes in its state

• writing a small test program to determine the meaning of some programming language construct, often while learning the language is using kind of operational semantics to determine the meaning of the construct.

• the change in the state of the machine defines the meaning of the statement

• depend on programming languages of lower levels, not mathematics

• to use operational semantics for a high-level language, a virtual machine is needed

• two different levels of uses of operational semantics

  • natural operational semantics
  • at the highest level, the interest is in the final result of the execution of a complete program
  • structural operational semantics
  • at the lowest level, operational semantics can be used to determine the precise meaning of a program through an examination of the complete sequence of state changes that occur when the program is executed

    Denotational Semantics

• most rigorous and most widely known formal method for describing the meaning of programs

• based on recursive function theory

• mathematical objects denote the meaning of their corresponding syntactic entities.

• the process of building a denotational specification for a language : defining a mathematical object for each language entity and a function that maps instances of the language entities onto instances of the corresponding mathematical objects

• syntactic domain : domain, semantic domain : range

• the meaning of language constructs are defined by only the values of the program's variables

• the state of a program is the values of all its current variables

• let VARMAP be a function that when given a variable name and a state, returns the current value of the variable

• since it's complex, it is of little use to language users

• provides an excellent way to describe a language precisely

  Axiomatic Semantics

• based on formal logic (predicate calculus)

• original purpose : formal program verification ( to prove the correctness of programs)

• Axioms and inference rules are defined for each statement type in the language to allow transformations of logic expressions into more formal logic expressions

• assertions : logic expressions

• precondition : an assertion before a statement that states the relationships and constraints among variables that are true at that point in execution

• postcondition : an assertion following a statement

• a weakest precondition : the least restrictive precondition that will guarantee the postcondition

• inference rule : a method of inferring the truth of one assertion on the basis of the values of our assertions. If S1, S2, S3, ..., Sn are all true then the truth of S can be inferred.

  • antecedent : the top part of an inference rule
  • consequent : the bottom part of an inference rule {P} statement {Q}

• axiom : a logical statement that is assumed to be true.

• the rule of consequence : if the logical statement {P} S {Q} is true, the assertion P' implies the aasertion {, and the assertion Q implies Q' then it can be inferred that {P'} S {Q'}

a = b + 1 (a > 1) one possible precondition : b > 10 weakest precondition : b > 0

sum = 2 * x + 1 (sum > 1) one possible precondition : x > 10 weakest precondition : x > 0

• if the precondition on the first statement is the same as the program specification, the program is correct.

  Assignment

weakest precondition P is defined by the axiom which means that P is computed as Q with all instances of x replaced by E.

Sequences

Selection

Logical Prestest Loops

Axioms