3
$\begingroup$

I am reading the book "Principle of Program Analysis" by Flemming Nielson for annotated type systems. In the first chapter, section 1.6 they mentioned the simple type system for various statements(S). And S maps a state to a state, and may therefore to have type Σ --> Σ where Σ denotes the type of state. So they mentioned a system of axioms and inference rules like below for sequential statements and if-else block:

  1. List item
  2. enter image description here

And later it is explained, an if-else statement in terms of Reaching Definition as below,enter image description here

Also, I can visualize the sequencing rule seems natural, but they mentioned conditional rule is more dubious. I am not able to understand how this is dubious? As per my understanding reaching definition after after 'if' block execution will may execute then block or else block, then how this is even conflicting? S1 may have different statements and S2 will also have different statements but these two blocks would not execute at same time. I am not getting this scenario, can you please help me with this

$\endgroup$
0
$\begingroup$

With the above expression, two branches (if and else) have the same analysis information at their respective entry and exit points i.e. In simple terms we can say that then-branch gives rise to the same set of reaching definitions as the else-branch does.

So, this is dubious, depending on the condition of if-block it is decided control will go to then or else block which will become the exit of if-block. To follow this idea we can modify the equation like below.

enter image description here

We assume that if if-block gets executed as true then final(S1) is executed i.e. RD2 and for false statement final(S2) i.e. RD3 is executed. The exit of the if-block is the subset of the union of then-block and the else-block.

enter image description here

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.