Semantics should be scoped

[MikaelMayer]

The semantics say that the following program executes correctly

if B {
  init x := 2;
} else {
  init x := 3;
}
assert x > 1;

This is because the small-step statement semantics inline the statements of a block when they are reached.
However, everyone I asked declared that this program should not be accepted because x is declared locally.
We need to make sure the semantics capture that.
This will be helpful to support shadowing because otherwise shadowing would not have been possible with this program:

init x := 2;
if B {
  init x := 3;
}
assert x == 2;

With shadowing semantics, this program verifies, but if the init of the blocks leaks, then this program no longer verifies.
I checked with many of us and we all agreed the program above, if given a meaning, it should be that x is shadowed, not overwritten.

[aqjune-aws]

This is right. With the 'current' syntax of Core, this type checks:

def shadowing :=
#strata
program Core;
procedure f(B : bool) returns () {
  var x: int;
  x := 2;
  if (B) {
    var x: int;
    x := 3;
  }
  assert x == 2;
};
#end