Contents (index)

• Notes on the Operational Semantics of Programming Languages
• : Outline
• : Natural_Operational_Semantics_of_While
• : Exercise 1
• : Exercise 2
• : Semantic Equivalence
• : Theorem 2.9 The NS are deterministic
• : Exercise 3
• : Semantic Function for the Natural Semantics of While
• : Hint: Semantic functions in ML
• : Exercise 4
• : Exercise 5
• : Structural Operational Semantics
• : Execution Sequences
• : Induction on Length of sequences
• : Derivation Sequence
• : Theorem SOS deterministic
• : Semantic function for structural operational semantics
• : Theorem NOS = S_SOS
• : Extensions to While
• : : while + abort
• : : while + non-determinism
• : : Exercise
• : : Exercise
• : : While + Parallelism
• : : Blocks
• : : Blocks with Procedures
• : : : Dynamic Scope for variables and procedures
• : : : Natural Semantics of Dynamic scoping
• : : : Exercise 2.38
• : : : Static Scope Rules for Procedures
• : : : Static Scope Rules for Variables
• : : : Static scopes for procedures and variables
• : Next: Provable Implementation
• Index of defined terms etc.

Notes on the Operational Semantics of Programming Languages

Outline

This page contains the formal systems that define various operational semantics of a simple programming language called While: [ intro.html ] and some of its extensions. They all make use of the syntax and semantics of simple While, numbers, variables, Arithmetic and Boolean Expressions:
1. BASIS::=
   Net{

   [ grammar_of_While in intro ] [ Semantics of Variables in intro ] [ Semantics of Expressions in intro ] [ Semantic equations for numbers in intro ] [ Semantics of Boolean Expressions in intro ]
   
   }=::BASIS.

   Natural_Operational_Semantics_of_While

2. NS::=following,
   Net
   Use syntax,state and arithmetic and boolean semantics [ BASIS ] For x:Var, a:Aexp, b:Bexp,s,s',s'':State,S,S1,S2:Stm.

   < S,s>->s' :: @=Executing statement S in state s leads to state s.

   
   

   1. |- (ass_ns): <x:=a,s>->s[x+>A[[a]]s].

      
      

   2. |- (skip_ns): <skip,s>->s.

      
      

   3. |- (comp_ns): if <S1,s>->s' and <S2,s'>->s'' then <S1;S2,s>->s''.

      
      

   4. |- (if_tt_ns): if B[[b]]s=tt and <S1,s>->s' then <if b then S1 else S2,s>->s'.

      
      

   5. |- (if_ff_ns): if B[[b]]s=ff and <S1,s>->s' then <if b then S1 else S2,s>->s'.

      
      

   6. |- (while_tt_ns): if B[[b]]s=tt and <S,s>->s' and <while b do S,s'>->s'' then <while b do S,s>->s''.

      
      

   7. |- (while_ff_ns): if B[[b]]s=ff then <while b do S,s>->s,

   
   (End of Net NS.)
   

   Note. One rule (shile_tt_ns) is not compositional,so proving general properties is not always a simple use of structural induction. Instead we induction on the derivation tree - showing that the proposition is true for all leaves in the tree (axioms) plus: if it is true for all smaller derivations (smaller trees) then it will be true ones with an extra step in the derivation.

   Note. You might say that the lack of structural inductive proofs leaves a loop hole that lets a 'while true do skip' statement escape being defined.

   Exercise 1

   Add a repeat construct to the syntax and semantics. Do not use 'while' to define the semantics!

   Exercise 2

   Add a for-loop construct to the syntax and semantics. Do not use 'while' to define the semantics!

   Semantic Equivalence

   S1 is equivalent to S2 iff for all s and s', <S1,s>->s' iff <S2,s>->s'.

   Theorem 2.9 The NS are deterministic

   For all S,s there is at must no more than one s' such that <S,s>->s'

   Exercise 3

   Prove that your [[repeat S until b]] is semantically equivalent to [[ S; while ~b do S]]. Hence show that your extended semantics are still deterministic.

   Semantic Function for the Natural Semantics of While

   Each statement is associated with a partial map from State into State.
3. S_NS::Stm -> (State <>->State).

4. S_NS[[S]] \in State <>->State.

5. If <S,s>->s' then S_NS[[S]] s = s' else undefined.

6. S_NS::= fun[S]( fun[s] ( the [s'](<S,s>->s').

   Notice that in all states s,

7. S_NS[[ while true do skip ]] s is undefined.

   Hint: Semantic functions in ML

   fun S_NS(S:Stm): (State -> State) = (fn(s)=> the s' such that <S,s>->s'). But how do you write
8. the s' such that <S,s>->s' in ML????

   Exercise 4

   Develop operational style semantics for Arithmetic expressions where
9. For z:Integer, a:Aexp,s:State, <a, s>->z::@=The final value of a in state s. So
10. <n,s>->N[[n]],

11. <x,s>->s x,

12. if <a1,s>->z1 and <a2,s>->z2 and z=z1+z2 then <a1+a2,s>->z.

    Complete the spec. Use structural induction on AExp to prove that gives the same meanings as the original semantics.

    Exercise 5

    Develop natural operational semantics for boolean expressions (Bexp) For t:{tt,ff}, b:Bexp,s:State, <b,s>->t::@=The final value of b in state s. Prove that your semantics defines the same function as the previous B[[_]] function.

    Structural Operational Semantics

    In Structural operational semantics we track both the state of the system and the computation yet to be done. When there is nothing left to be done the computation terminates.

13. Possible_statement::=O(Stm).
14. PES::=Partially_executed_state::= <Possible_statement,State >. A relation(=>) is defined on these partially executed states that holds if one can change to another: For S,S': Stm, s,s':State, <S,s> => <S',s'>::@=In one step S in state s becomes S' in state s'.

15. Terminal_state::= <empty, State>. Normally abbreviate the terminal state <empty, s> as s.

16. SOS::=following,
    Net
    Use syntax,state and arithmetic and boolean semantics [ BASIS ] For x:Var, a:Aexp, b:Bexp,s,s',s'':State,S,S1,S2:Stm.

    
    

    1. |- (ass_sos): <x:=a,s> =>s[x+>A[[a]]s].

       
       

    2. |- (skip_sos): <skip,s> =>s.

       
       

    3. |- (comp_1_sos): if <S1,s> =><S3,s'> then <S1;S2,s>=><S3;S2,s'>.

       
       

    4. |- (comp_2_sos): if <S1,s> =>s' then <S1;S2,s>=><S2,s'>.

       
       

    5. |- (if_tt_sos): if B[[b]]s=tt then <if b then S1 else S2,s> =><S1,s>.

       
       

    6. |- (if_ff_sos): if B[[b]]s=ff then <if b then S1 else S2,s> =><S2,s>.

       
       

    7. |- (while_sos): <while b do S,s> =><if b then (S; while b do S)else skip,s>.
    
    (End of Net SOS.)
    

    The last rule is not compositional (why?) and so we can not use induction on the syntactic structure to prove properties of the system. Instead it is possible to use induction on the number of steps taken as the processing evolves - see induction on the length of the derivation sequence below.

    Execution Sequences

    If for no \gamma:Partially_executed_state, <S,s>=>\gamma, then <S,s> is stuck.

17. Stuck::={<S,s> || for no \gamma:Partially_executed_state(<S,s>=>\gamma }.

    An execution sequence is a (possibly infinite) series of partially executed states(\gamma(0), \gamma(1), ...) where each <S,s> leads to the next one:

    Series are defined on sequences of adjacent natural numbers starting with 0:

18. Interval::= {Empty} | Finite_interval | {Nat0}, where
19. Finite_interval::={ 0..n | for some n:Nat0 }.

20. For N:Interval, Execution::@(N->PES)= { \gamma:N->PES|| for all i:pre(\gamma)-{0} ( \gamma[i-1] => \gamma[i]
    }.

Induction on Length of sequences

Suppose we have a series where adjacent items satisfy a relation R: