Consider a restricted while loop. In a restricted while loop, all updates to the variables used in the condition must occur in the loop condition and don't affect the loop body. Furthermore, these updates are not reflected in any code that occurs after the loop terminates. Updates that occur in the loop body both affect the loop body and code that occurs after the loop, but updates in the loop body don't affect the loop condition. For example:

int i $=0$;

restrictedwhile $($i$++<10)\{$

i $=$ i $-1$;

int x $=$ i;

$\}$

Because the loop condition and the loop body don't affect each other, the value stored in x will be $-10.$ The increment of i only affects the loop condition. The decrement of i affects both the loop body and the code that occurs after the loop ends.

Give the denotational semantics for such a restricted while loop.