инициализация массива с помощью функции

Question

method arrayFromSeq<T(0)> (s: seq<T>) returns (a:array<T>)
    ensures a[..] == s
    ensures fresh(a)
{
// a := new T[|s|]; 
//forall i | 0 <= i < |s| { a[i] := s[i]; }
a := new T[|s|] (i => (s[i]));
}

Я хотел бы заменить первые две строки в теле третьей строкой, чтобы избежать квалификатора (0) в типе T, но при этом возникает ошибка «индекс вне диапазона».

Answer 1

Вы можете использовать эту модифицированную версию третьей строки вместо

a := new T[|s|] (i requires 0 <= i < |s| => s[i]);

Причина, по которой ваша версия третьей строки не работает, заключается в том, что Dafny проверяет анонимные функции отдельно от их контекста. Глядя на изолированную функцию i => s[i], Дафни обеспокоен тем, что i может выйти за пределы.

Исправление состоит в том, чтобы ввести предварительное условие для этой анонимной функции, что я и показал выше. Теперь, глядя на функцию изолированно, предварительное условие гарантирует, что индекс будет в границах.

Отдельно, Дафни должен проверить, удовлетворяется ли это предварительное условие использованием функции. Эта проверка проходит, потому что Дафни знает, что инициализация массива new T[|s|] будет вызывать функцию только с аргументами от 0 до |s|.