Block rule in small step?

[lohner]

For the program {var a := 0; a := 1; a := 2}, the execution trace looks like this at the moment:

〈{var a = 0; a := 1; a := 2}, σ0〉   
→1 〈{var a = 0; skip; a := 2}, σ2〉
→1 〈{var a = 0; a := 2}, σ2〉
→1 〈{var a = 0; skip}, σ3〉
→1 〈{var a = 2; skip}, σ4〉
→1 〈skip, σ4〉

However rule Block1 suggests that it shoud read like this:

〈{var a = 0; a := 1; a := 2}, σ0〉   
→1 〈{var a = 1; skip; a := 2}, σ2〉
→1 〈{var a = 1; a := 2}, σ2〉
→1 〈{var a = 2; skip}, σ3〉
→1 〈skip, σ3〉

Note the 𝒩^{-1} in the rule.

[parttimenerd]

Thanks for your comment. One question: Is your last step correct? Or can you explain why it shouldn't result into →₁ 〈skip, σ₄〉?

[parttimenerd]

The current implementation outputs the following

〈{var a = 0; a := 1; a := 2; c := 4}, σ₀〉   
→₁ 〈{var a = 5; skip; a := 2; c := 4}, σ₀〉
→₁ 〈{var a = 5; a := 2; c := 4}, σ₀〉
→₁ 〈{var a = 5; skip; c := 4}, σ₀〉
→₁ 〈{var a = 5; c := 4}, σ₀〉
→₁ 〈{var a = 0; skip}, σ₂〉
→₁ 〈skip, σ₂〉

Is this the correct behaviour that you expected?

[parttimenerd]

This a bigger problem than I originally thought. It's easy to comprehend but hard to implement (much harder than the Seq rule).