По поводу призраков:

[kouzdra]

Кажется не все въезжают, "о чем это":

ghost var prevElements := a[..];
while // ...
invariant a[lo..hi] == prevElements[lo..hi];
{
// ...
}
ghost var нужны имено для задания инвариантов без порождения лишнего кода. С точки зрения компилятора они ведут так же как обычные и на общих правах участвую в процессе верификации "как если бы были настоящими" - но в код это не попадает.

Аналогом этого кода в С было бы что-то вроде:

std::vector a = ...
...
auto const inv = std::vector (a [lo], a [hi]);
for (int i = 0; i != a.size(); ++ i) {
assert (inv == std::vector (a [lo], a [hi]));
...
}
Только без оверхеда и с контролем условия во время компиляции