CSE411: Introduction to Compilers

Formal Semantics

Jooyong Yi (UNIST)

Specifications

• Specifications are useful.

           regular expression
                    ↓
             |-------------|    
             |    Lexer    |        
             | Synthesizer |
             |-------------|
                    |
               synthesizes   
                    ↓
                |-------|            
int val = 10; → | Lexer | → int ID ASSIGN NUM ;
                |-------|                          

Specifications

• Specifications are useful.

                  CFG
                   ↓
            |-------------|    
            |    Parser   |        
            | Synthesizer |
            |-------------|
                   |
              synthesizes   
                   ↓
              |--------|            
    program → | Parser | → ok / error
              |--------|                          

Specification of Semantics?

Specification of Semantics?

• Type checking

   Γ ⊢ I:τ  Γ ⊢ E:τ       # premises
----------------------
      Γ ⊢ I = E           # conclusion  

class Visitor extends ASTVisitor {
  ...
  public boolean visit(final Assignment node) {
    node.getLeftHandSide().accept(this);
    final Type lhsType = getResult();
    node.getRightHandSide().accept(this);
    final Type rhsType = getResult();
    if (lhsType != rhsType) {
      throw new Error(node, "Type mismatch in \"" + node + "\": " + lhsType + " = " + rhsType);
    }
    return false;
  }
  ...
}  

Operational Semantics Example

• Consider the following if statement:

if b S1 S2

• b: boolean expression
• S1: the statement to be executed if b is true
• S2: the statement to be executed if b is false

Operational Semantics Example

   ⟨S1, s⟩ → s'
---------------------- if B⟦b⟧(s) = true
 ⟨if b S1 S2, s⟩ → s'


   ⟨S2, s⟩ → s'
---------------------- if B⟦b⟧(s) = false
 ⟨if b S1 S2, s⟩ → s'

Operational Semantics: Transition Relation

⟨S1, s⟩ → s'

Executing statement S1 in state s results in state s'.

   ⟨S1, s⟩ → s'                             # premise
---------------------- if B⟦b⟧(s) = true
 ⟨if b S1 S2, s⟩ → s'                       # conclusion

B⟦b⟧(s) represents the value of b when evaluated in state s.

Implementing Operational Semantics

   ⟨S1, s⟩ → s'                                   ⟨S2, s⟩ → s'
---------------------- if B⟦b⟧(s) = true       ---------------------- if B⟦b⟧(s) = false
 ⟨if b S1 S2, s⟩ → s'                           ⟨if b S1 S2, s⟩ → s'

let rec execute : cmd -> state -> state
= fun c s -> match c with 
   | ...
   | If (b, c1, c2) -> if eval b s then execute c1 s else execute c2 s
   | ...

Implementing Operational Semantics (While Statement)

  ⟨S, s⟩ → s'      ⟨while b S, s'⟩ → s''
----------------------------------------- if B⟦b⟧(s) = true    ------------------------- if B⟦b⟧(s) = false
           ⟨while b S, s⟩ → s'                                   ⟨while b S, s⟩ → s

let rec execute : cmd -> state -> state
= fun c s -> match c with 
   | ...
   | If (b, c1, c2) -> if eval b s then execute c1 s else execute c2 s
   | While (b, c) -> if eval b s then execute (While (b,c)) (execute c s) else s
   | ...

Operational Semantics (Sequence)

  ⟨S1, s⟩ → s'   ⟨S2, s'⟩ → s''
----------------------------------
       ⟨S1;S2, s⟩ → s''

Operational Semantics (Assignment)

------------------------------
   ⟨x = a, s⟩ → s[x ↦ A⟦a⟧(s)]

• A⟦a⟧(s) represents the value of a when evaluated in state s.
• s[x ↦ v] represents the state s where the value of x is updated to value v.