Operational semantics - A simple imperative language.

Martin Sulzmann

Overview

From syntax to semantics

Consider the following code snippets.

        b := f1()

        if b {
        fmt.Printf("Hi")
        } else {
        fmt.Printf("Ho")
        }
        if f1() && f2() {
        fmt.Printf("Hi")
        } else {
        fmt.Printf("Ho")
        }
    go func() {
        fmt.Printf("Hi")
    }()

    go func() {
        fmt.Printf("Hi")
    }()

What happens during execution?

Observation: Execution depends on

What could happen versus what actually has happened

Given some program P we wish to answer the following questions:

We will introduce operational semantics rules to specify the possible execution behavior of programs.

Later we discuss how to record the execution behavior of programs for analysis purposes.

EXP: A simple expression language

We specify the operational semantics of a simple (Boolean) expression language.

Syntax

We make use of the EBNF notation to describe the abstract syntax of expressions.

 B ::= true | false

 E ::= B | !E | E && E

Semantics

We make use of operational semantics rules to formally specify the execution of expressions.

Rules are of the form

E => B

and reads as follows: “Expression E evaluates to the value B”.

For each expression pattern as described by the above syntax, we define an operational semantics rule.

Boolean constants

(B-1)  true => true

(B-2)  false => false

Boolean constants evaluate to itself.

Compound expressions

Consider Boolean conjunction.

We write E1 && E2 to denote an expression that involves Boolean conjunction where E1 refers to the left operand and E2 refers to the right operand.

What is the result of evaluating E1 && E2?

The common evaluation rules applied in programming languages are as follows:

Via operational semantics rules we can precisely specify such evaluation rules.

          E => true
(Not-1)  -------------
          !E => false

          E => false
(Not-2)  -------------
          !E => true


           E1 => false
(And-1)   -----------------
           E1 && E2 => false

           E1 => true
           E2 => false
(And-2)   -----------------
           E1 && E2 => false

           E1 => true
           E2 => true
(And-3)   -----------------
           E1 && E2 => true

Above rules shall be interpreted as “if-then” rules. The part above the --------- is the precondition (premise) and the part below is the postcondition (conclusion).

If

then

Consider an example where we evaluate true && !true

                                       (B-1) true => true
                              (Not-1) --------------------------
       (B-1) true => true             !true => false

(And-2)  --------------------------
          true && !true => false

We obtain an evaluation tree. Evaluation rules are syntax-directed. We traverse the structure of expressions and apply the respective rules. Leaf nodes correspond to evaluation of constants and intermediate nodes correspond to evaluation of compound expressions.

Here’s some Go implementation that “literally” implements the above semantics.

The above form of operational semantics rules are commonly referred to as “big-step” evaluation rules.

SIMP: A simple imperative language

We consider an extension of Exp that includes some imperative programming features.

Syntax

 B ::= true | false

 V ::= "x" | ...                  // Variables

 E ::=  B | !E | E && E | V


 Stmt ::= if E then Stmt else Stmt         // Conditional statement
    |  V = E                               // Assignment
    |  print V                             // print
    |  Stmt ; Stmt                         // Sequence of statements

There are no types. We assume that SIMP is an untyped language.

Semantics

Due to the presence of variables, we require an additional component that keeps track of the values assigned to variables.

S ::= [] | [V : B] | S + S

We write V : B to denote that variable V is assigned to the value B. We use lists to record the value assignment for variables. For example, consider [V_1 : B_1, ..., V_n : B_n]. We refer to S as the value state of variables.

We assume a lookup function to lookup the value of variable V in S. The definition of lookup is as follows.

lookup([V_1 : B_1, ..., V_n : B_n],V) = B_i

   if V_i = V and forall j < i we have that V_j != V


lookup([V_1 : B_1, ..., V_n : B_n],V) = undefined

   if V_i != V for all i

In case there are several value assignments for the same variable, we pick the earlier assignment.

Evaluation of expressions

The operational semantics rules have now as an additional parameter the value state S. We write S |- E => B to denote that under value assignment S, expression E evaluates to B.

          lookup(S,V) = B
         ----------------
(Var-1)     S |- V => B

          lookup(S,V) = undefined
         ----------------
(Var-2)     S |- V => false

          S |- E => true
(Not-1)  -------------
          S |- !E => false

          S |- E => false
(Not-2)  -------------
          S |- !E => true

           S |- E1 => false
(And-1)   -----------------
           S |- E1 && E2 => false

           S |- E1 => true
           S |- E2 => false
(And-2)   -----------------
           S |- E1 && E2 => false

           S |- E1 => true
           S |- E2 => true
(And-3)   -----------------
           S |- E1 && E2 => true

Evaluation of statements

Operational semantics rules to describe statements are of the form

(S,Stmt) => S'

and reads as follows: “Evaluate Stmt under value assignment S and obtain a new value assignment S’”.


        (S, Stmt_1) => S'    (S', Stmt_2) => S''
(Seq)  --------------------------------------------
        (S, Stmt_1 ; Stmt_2) => S''


           S |- E => true   (S,Stmt_1) => S'
(Ite-1)  --------------------------------------
          (S, if E then Stmt_1 else Stmt_2) => S'


           S |- E => false   (S,Stmt_2) => S'
(Ite-2)  --------------------------------------
          (S, if E then Stmt_1 else Stmt_2) => S'


           S |- E => B   S' = [V:B] + S
(Assign)  ----------------------------
           (S, V = E) => S'

           S |- V => B     "print B onto the console"
(Print)  ---------------------------------------------
           (S, print V) => S

In case of (Assign) we obtain a new value assignment. The new value binding V:B is put at the beginning and by definition of lookup guarantees that we always retrieve the latest updates.

Here’s some Go implementation that implements SIMP evaluation rules.