Ghost Variables

Is re-declaration of a ghost variable in inner loop’s _term allowed, considering multiple nested scopes?
Is a local/global variable allowed to share the same name of a ghost variable?

No, it is not, because this does not re-declare the variable, but instead create a new one that shadows the old one.

The following example is valid code, but the inner variable shadows the ghost variable:

while(0) _Invariant(1) _Term(0; k) {
  int k = 0;
  k = k + k;
}

The idea is that you should be able to remove invarians and termination conditions and still get a valid program.

May I then assume that “in general, for each loop there is at most one ghost variable declaration” ?

How would a loop with several such declarations look like?

1 Like
while(condition) _Invariant(1) _Term(0; k) {
  int k = 0;
  while(0) _Invariant(k) _Term(0; l) {
      k = k + k;
  }
}

So, in this example a k in the inner invariant is shadowed by the local declaration, isn’t it?

Yes, in that example, the k in the invariant refers to the k that is set to 0 in the line int k = 2; This is allowed to happen, we would expect your code to generate a formula here.

1 Like