Slide 9.9: A control example (cont.)

Slide 9.8: A control example
Slide 10.1: Axiomatic semantics
Home

A Control Example (Cont.)

     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

Reduce the statement “i ':=' i '–' '1'”:

   <i ':=' i '–' '1' | {n=-3, i=3, fact=3}>
⇒ <i ':=' 3 '–' '1' | {n=-3, i=3, fact=3}>  (Rules 15 and 8)
⇒ <i ':=' 3 '–' 1 | {n=-3, i=3, fact=3}>    (Rules 1 and 11)
⇒ <i ':=' 2 | {n=-3, i=3, fact=3}>          (Rules 4 and 17) 
⇒ {n=-3, i=3, fact=3} & {i=2}               (Rule 16)
=  {n=-3, i=2, fact=3}

Therefore,

   <'while' i 'do' … 'od' | {n=-3, i=3, fact=1}>
⇒ <fact ':=' fact '*' i;  i ':=' i '–' '1';
     'while' i 'do' … 'od' | {n=-3, i=3, fact=1}>  (Rule 24)
⇒ <i ':=' i '–' '1';  'while' i 'do' … 'od' |
     {n=-3, i=3, fact=3}>                          (Rule 18)
⇒ <'while' i 'do' … 'od' | {n=-3, i=2, fact=3}>    (Rule 18)

Continuing in this way, we get

   <'while' i 'do' … 'od' | {n=-3, i=2, fact=3}>
⇒ <'while' i 'do' … 'od' | {n=-3, i=1, fact=6}>
⇒ <'while' i 'do' … 'od' | {n=-3, i=0, fact=6}>

When the variable i reaches to the value 0:

   <'while' i 'do' … 'od' | {n=-3, i=0, fact=6}>
⇒ {n=-3, i=0, fact=6}                           (Rule 23)

So the final environment is {n=-3, i=0, fact=6}.