Еще про ghost в Dafny

В tutorial'ах по Dafny написано, что ghost можно объявить локальную переменную, поле класса, метод класса. Но, оказывается, можно объявить и возвращаемое значение ghost. Это помогает избежать ненужных кванторов существования и повысить эффективность автоматического доказательства. Каким же образом. Представим, что пишется метод, вычисляющий максимум в непустом массиве. В его постусловии будет записано, что существует такое число в границах индексов массива, что возвращаемый максимум является элементом массива с индексом по этому числу. Но ведь в коде метода и так вычисляется этот индекс, а в постусловии по сути лишний раз записываются свойства этого индекса. Двойную работу можно попытаться снять, объявив этот индекс ghost возвращаемым значением! И тогда постусловие станет проще: из него уйдет квантор существования:

method max(a : array) returns (m : int, ghost ind : nat)
requires a != null;
requires a.Length > 0;
ensures 0 <= ind < a.Length; ensures m == a[ind]; ensures forall i :: 0 <= i < a.Length ==> m >= a[i];
{
ind := 0; m := a[0];
var i := 1;
while (i < a.Length) invariant 0 < i <= a.Length; invariant 0 <= ind < a.Length; invariant a[ind] == m; invariant forall j :: 0 <= j < i ==> m >= a[j];
{
if (a[i] > m) { m := a[i]; ind := i; }
i := i + 1;
}
}

method main(a : array)
requires a != null;
requires a.Length > 0;
{
var mm, i := max(a);
}