Slide 9.8: A control example

A Control Example

As an example, let us reduce the while-statement of the program:

     n := 0 – 3;
     if  n  then  i := n  else  i := 0 – n  fi;
     fact := 1;
     while  i  do
        fact := fact * i;
        i := i – 1
     od

to its environment value. The environment at the start of the while-loop is {n=-3, i=3, fact=1}. Rule 24 applies

             <E|Env> ⇒ <V|Env>, V>0             
 <'while' E 'do' L 'od' | Env> ⇒ 
       <L ; 'while' E 'do' L 'od' | Env>

because

   <i | {n=-3, i=3, fact=1}> ⇒ <3 | {n=-3, i=3, fact=1}>

and 3 > 0. By Rule 18,

         <S|Env> ⇒ Env₁         
 <S ';' L | Env> ⇒ <L | Env₁>

we must compute the environment resulting from the application of the body of the loop to the environment {n=-3, i=3, fact=1}:

   <fact ':=' fact '*' i | {n=-3, i=3, fact=1}>
⇒ <fact ':=' 1 '*' i | {n=-3, i=3, fact=1}> (Rules 15 and 9) 
⇒ <fact ':=' 1 '*' 3 | {n=-3, i=3, fact=1}> (Rules 15 and 12)  
⇒ <fact ':=' 3 | {n=-3, i=3, fact=1}>       (Rules 5 and 17) 
⇒ {n=-3, i=3, fact=1} & {fact=3}            (Rule 16)
=  {n=-3, i=3, fact=3}

Update the environment from {n=-3, i=3, fact=1} to

{n=-3, i=3, fact=3}: 
 
   <fact ':=' fact '*' i; i ':=' i '–' '1'|{n=-3,i=3,fact=1}>
⇒ <i ':=' i '–' '1' | {n=-3, i=3, fact=3}>   (Rule 18)