Semantics of C0


Regarding the 6th chapter “The Semantics of C0”, I’d like to discuss 5 points.

  1. In Subsection 6.3.1, it is mentioned that the memory assignment, 𝜇 : Addr ⇀ Val U {?}, is a partial mapping, despite the 2 facts (the codomin is Val U {?} and every experission is either defined or undefined). Why is the memory assignment still partial?

  1. In defintion 6.3.7, it is said that

“If there is no state under which 𝑠 terminates, then we say that 𝑠 diverges.”

So, shouldn’t we say that

“if there is no configuration under which 𝑠 terminates, then we say that 𝑠 diverges.”?

Otherwise, the definiton of divergence will overlap with termination in case of abortion or getting stuck.

  1. In Example 6.3.9, the listing below:
    Would it also be a bit more accurate if we add the assignment li $t0 42 (in MIPS prg, line 2) after the label L1?

  1. In Example 6.3.10, some typos.

  1. In Example 6.3.12,
    Since the statement S is a Block contains two Assignemnts, the configuration 5 (numbers shown next to the configuration in the snapped image) should be
    <{{ {r=r-y; q=q+1;} while (y<=r)S }} | state > rather than <{{r=r-y; q=q+1; while (y<=r)S }} | state >?
    If “Yes”, then we need to
  • use the [Subst] rule twice instead of once.
  • after excuting both assignments of S (before line 7), add a configuration for the empty block. For example: <{{ {} while (y<=r)S }} | state > -> <{{ {} while (y<=r)S }} | state > using [Empty], [Exec], [Subst].

Same case for configuration 9.

Moreover, I think, some rules used for the last configurations with respect to [Empty] are either missed or redundant.

1 Like
int x;
int y;
// here

Let’s say the address of x is \triangle and \square for y.
The memory assignment is \{\triangle\mapsto 3, \square\mapsto ?\}.
Therefore, x is defined, y is undefined, and \circ is not in the domain as this memory is not in use.

Yes, divergence is if the program does not terminates. Therefore, it should be configuration here.

It depends on the compiler.
A good compiler would not load 42 twice.
Your compiler (project 6) will probably use even more instructions than shown here.
In the example, the concrete code is not relevant, only its semantics.

We will fix it, thanks.

Yes, indeed the body of the while is a block itself and needs another nesting.

What do you mean?

1 Like

Thank you for the fast response.

  1. I should’ve thought about the domain.
  1. But should the compiler also care about the case that the assignment of $t0 is not reached when y!=0? An alternative might be to do this assignment first.

Here, I mean, the rules used for the last 4 configurations (line 14 to 17) might be accurately written as edited in the snapped picture.

You are right, if it jumps to L2 and then to L1, t0 contains the wrong content.
The fix would indeed be to first load 42 into t0.


1 Like