[CSUSB] >> [CompSci] >> [Dick Botting] >> [CS620 Course Materials] >> operational
[Index] || [Contents] Mon Apr 14 15:51:46 PDT 2003

Contents (index)


    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::=
    }=::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:

  • g0 R g1 R g2 R ... R g[n] The we know that when
  • (1) property is true of g0 and
  • (2)For all i, If it is true of g[i] then it true of g[i+1], then that property holds for all of them.

    Induction on the length of a sequence is slightly subtler than this. The elements are in fact series and we are interested in properties of the whole sequence:

  • g0: Empty

  • g1: \gamma[0]

  • g2: \gamma[0] R \gamma[1]

  • g3: \gamma[0] R \gamma[1] R \gamma[2]

  • ...

    Derivation Sequence

    A derivation sequence is any finite execution ending in a stuck or terminal state or any infinite execution sequence.

    Intuitively we expect the infinite and stuck sequences to occur in cases were the equivalent natural semantics fail to define a final state.

    Theorem SOS deterministic

    The structural Operational semantics are deterministic.

    Semantic function for structural operational semantics

    We say that S_SOS[[S]]s = s' iff a finite derivation sequence leads from <S,s> to s'. For S:Stm, s,s':State, S_SOS[[S]]s = s' iff for some n, <S,s>=>^n <empty,s'>.

    Theorem NOS = S_SOS

    Natural and structural operational semantics are equivalent

    Extensions to While

    while + abort

  • Stm::= BASIC.Stm | abort.
  • NS_AB::=
    Net{
      |NS.
    1. |- (ab_ns): For no s,s', <abort,s>->s' .

    }=::NS_AB.

  • SOS_AB::=
    Net{

    1. |-SOS.
    2. |- (ab_sos): For no S',s,s' <abort,s> => <S',s'> .

    }=::SOS_AB.

    while + non-determinism

  • Stm::= BASIC.Stm | S1 or S2.

  • NS_ND::=
    Net{

    1. |-NS.
    2. |- (or_1_ns): if <S1,s>->s' then <S1 or S2,s>->s'.
    3. |- (or_2_ns): if <S2,s>->s' then <S1 or S2,s>->s'.

    }=::NS_ND.

  • SOS_ND::=
    Net{

    1. |-SOS.
    2. |- (or_1_sos): <S1 or S2,s>=><S1,s>.
    3. |- (or_2_sos): <S1 or S2,s>=><S2,s>.

    }=::SOS_ND.


  • (above) |- In NS nondeterminism will suppress a loop (angelic!)


  • (above) |- In SOS nondeterminism does not suppress a loop (demonic!)

    Exercise

    x:=-1; while x<=0 do ( x:=x-1 or x::=(-1)*x) What are the possible final states according to NS. What derivation sequences are specified by SOS. Does NS and SOS give the same meaning to this program?

    Exercise

  • Stm::= BASIC.Stm | random(x). Can change x to any positive natural number in n unpredictable way ("randomly"). Extend NS and SOS to express this. In each case can "or" do the same job and random?

    While + Parallelism

    Interleaved: Some sequence of statements from S1 and S2 are executed.

  • Stm::= BASIC.Stm | S1 par S2.
  • SOS_Par::=
    Net{

    1. |-SOS.
    2. |- (par_1_sos): if <S1,s>=><S1',s'> then <S1 par S2,s>=><S1' par S2,s'>.
    3. |- (par_2_sos): if <S1,s>=>s' then <S1 par S2,s>=><S2,s'>.
    4. |- (par_3_sos): if <S2,s>=><S2',s'> then <S1 par S2,s>=><S1 par S2',s'>.
    5. |- (par_4_sos): if <S2,s>=>s' then <S1 par S2,s>=> <S1,s'>.

    }=::SOS_Par.

    Suppose{

  • |- (par_1_ns): if <S1,s>->s' and <S2,s'>->s'' then <S1 par S2,s>->s''.
  • |- (par_2_ns): if <S1,s>->s' and <S2,s'>->s'' then <S1 par S2,s>->s''.

    No. Not interleaving.... the whole of one and then the other, or vice versa.
    }.

    Natural semantics avoids defining steps in a computation and so has a built in problem with expressing the idea of interleaving the steps in two computations.

    Blocks

  • Stm::=BASIC.Stm | begin #Dcl Stm end.
  • Dcl::=declaration of a local variable.
  • Dcl::abstract_syntax= var Var = Aexp.

    For D:#Dcl.

    Define effect of declarations in terms of

  • <D,s>->s' and new operation on states that overlays a whole set of variables X with new values. For s1,s2:State, X:Sets(Var), x:Var, (s1[X+->s2]) x ::= if x \in X then s2 x else s1 x.

    Also need the set of variables defined by a sequence of declarations

  • For D:#Dcv, DV(D)::Sets(Var)=Set of variables declared in D,
  • DV("")::={},
  • DV(var x:=a; D)::={x}|DV(D).

  • BLOCK::=
    Net{

    1. |-NS.
    2. |- (block_ns): if <D,s>->s' and < S,s' >->s'' then <begin D S end,s>->s'[DV(D)+->s],

    }=::BLOCK.
  • VAR::=
    Net{

    1. |- (var_ns): if <D,s[x+>A[[a]]s]>->s' then <var x:=a; D,s>->s'.
    2. |- (none_ns): if <"",s>->s.

    }=::VAR.

    Blocks with Procedures

  • Stm::=BASIC.Stm | begin #Dcv #Dcp Stm end | call Pname.
  • Dcv::=declaration of a local variable.
  • Dcp::=declaration of a local procedure.
  • Pname::=Name of procedure declared in outer block...::Sets(Pname).

    For Dv:#Dcv, Dp:#Dcp.

    Dynamic Scope for variables and procedures

  • EnvP::=Pname->Stm.

    For p:Pname,S:Stm, (p+>S) in EnvP iff Procedure p has a body S.

    The environment is kept up to date by

  • upd::#Dcp><EnvP->EnvP=Update (2nd) by procedure declarations (1st),
  • upd("", e)::=e,
  • upd(proc p is S; Dp, e)::=upd(Dp, e[p+>S]) Natural Semantics using the Environment

    For e:EnvP,S:Stm,s,s':State, (e|-<S,s>->s')::@=`In environment e, and state s, statement S leads to s'

    Natural Semantics of Dynamic scoping

  • NS_DYN_V_P::=
    Net{
      Use syntax,state and arithmetic and boolean semantics [ BASIS ] [ VAR ] For x:Var, a:Aexp, b:Bexp,s,s',s'':State,S,S1,S2:Stm, Dv:#Dcv, Dp:#Dcp, ep:EnvP.

      (<ep, S,s>->s')::@=`In environment ep, and state s, statement S leads to s'.


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


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


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


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


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


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


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


    8. |- (block_dvp_ns): if <Dv,s>->s' and <udp(Dp,ep), S,s' >->s'' then <ep,begin Dv Dp S end,s>->s'[DV(Dv)+->s].


    9. |- (call_rec_dvp_ns): if <ep, ep(p),s>->s' then <ep,call p,s>->s'.


    }=::NS_DYN_V_P.

    Exercise 2.38

    Static Scope Rules for Procedures

    EnvP = Pname <>-> (Stm ><EnvP ). Note: this is recursive... but we only ever have Environments constructed by a finite number of nested constructions - Each procedure points back to its parents environment...

    For ep:EnvP, p:Pname, if p in pre(ep) then

  • env(ep,p)::= 2nd(ep(p)),
  • stm(ep,p)::=1st(ep(p)).

  • NS_DYN_V_S_P::=
    Net{
      [ NS_DYN_V_P ] without (call_rec_dvp_ns).
    1. |- (call_dvsp_ns): if env(ep,p)|-<stm(ep,p),s>->s' then ep|-<call p,s>->s'.
    2. |- (call_dvsp_rec_ns): if env(ep,p)[p+>ep(p)]|-<stm(ep,p),s>->s' then ep|-<call p, s>->s'

    }=::NS_DYN_V_S_P.

    Static Scope Rules for Variables

    EnvV = Var->Loc. Store= Loc | { next } -> Z.

  • new::Loc->Loc.
  • For all n:Nat, l:Loc(not( Loc^n(l) = l ) ).

  • NS_V_Loc::=
    Net{
      For ev,ev':EnvV, sto,sto':Store, Dv:#Dcv, l:Loc, v:Integer.
    1. |- (var_loc_ns): For v:=A[[a]](sto o ev) and l := sto next, if <Dv, ev[x+>l], sto[l+>v][next+>new l]>->(ev', sto') then < var x:=a; Dv, ev, sto>->(ev', sto').
    2. |- (none_loc_ns): <"", ev, sto>->(ev,sto).

    }=::NS_V_Loc.

    Static scopes for procedures and variables

  • EnvP::=Pname<>->Stm>< EnvV><EnvP.

    For Dp:#DcP, ev:EnvV, ep:envP,

  • udsp(proc p is S; Dp, ev, ep)::EnvP=udsp(Dp, ev,ep[p+>(S,ev,ep)]),
  • udsp("", ev,ep)::=ep.

  • NS_S_V_P::=
    Net{
      For ep:EnvP, ev:EnvV, sto,sto':Store, (ev,ep|-<S,sto>->sto')::@=`with store sto with variables ev and procedures ep,S leads to store sto'`.

      For x:Var, a:Aexp, b:Bexp,s,s',s'':State,S,S1,S2:Stm, Dv:#Dcv, Dp:#Dcp, ep:EnvP, ev:EnvV, sto,sto',sto'':Store.


    1. |- (ass_svp_ns): ev,ep|-<x:=a,sto>->sto[ev x+>A[[a]](sto o ev)].


    2. |- (skip_svp_ns): ev,ep|-<skip,sto>->sto.


    3. |- (comp_svp_ns): if ev,ep|-<S1,sto>->sto' and ev,ep|-<S2,sto'>->sto'' then ev,ep|-<S1;S2,sto>->sto''.


    4. |- (if_tt_svp_ns): if B[[b]](sto o env)=tt and ev,ep|-<S1,sto>->sto' then ev,ep|-<if b then S1 else S2,sto>->sto'.


    5. |- (if_ff_svp_ns): if B[[b]](sto o env)=ff and ev,ep|-<S1,sto>->sto' then ev,ep|-<if b then S1 else S2,sto>->sto'.


    6. |- (while_tt_svp_ns): if B[[b]](sto o env)=tt and ev,ep|-<S,sto>->sto' and ev,ep|-<while b do S,sto'>->sto'' then ev,ep|- <while b do S,sto>->sto''.


    7. |- (while_ff_svp_ns): if B[[b]](sto o env)=ff then ev,ep|-<while b do S,sto>->sto.


    8. |- (block_svp_ns): if <Dv,ev, sto>->(ev',sto') and ev', udsp(Dp,ev',ep)|-< S,sto' >->sto'' then ev',ep'|-<begin Dv Dp S end,sto>->sto''.


    9. |- (call_svp_ns): For (S,ev',ep'):=ep(p), if ev',ep'|-<S,sto>->sto' then ev,ep|-<call p,sto>->sto'.


    10. |- (call_rec_svp_ns): For (S,ev',ep'):=ep(p), if ev',ep'[p+>ep(p)]|-<S,sto>->sto' then ev,ep|-<call p,sto>->sto'.


    }=::NS_S_V_P.

    . . . . . . . . . ( end of section Blocks and Procedures) <<Contents | Index>>

    . . . . . . . . . ( end of section Extensions to While) <<Contents | Index>>

    Next: Provable Implementation

    To Be Announced

    . . . . . . . . . ( end of section Notes on the Operational Semantics of Programming Languages) <<Contents | Index>>


    Formulae and Definitions in Alphabetical Order