Удивительно, дафни не удалось проверить ограниченность заданного понимания

Question

У Дафни нет проблем с этим определением функции пересечения множеств.

function method intersection(A: set<int>, B: set<int>): (r: set<int>)
{
    set x | x in A && x in B
}

Но когда дело доходит до объединения, Дафни жалуется, "понимание набора должно производить конечный набор, но эвристика Дафни не может понять, как создать ограниченный набор значений для" х "". A и B конечны, и поэтому, очевидно, объединение тоже.

function method union(A: set<int>, B: set<int>): (r: set<int>)
{
    set x | x in A || x in B
}

Чем объясняется это, на первый взгляд, несоответствующее поведение?

Answer 1

Это действительно потенциально удивительно!

Во-первых, позвольте мне отметить, что на практике у Дафни есть встроенные операторы для пересечения и объединения, которые, как он знает, сохраняют конечность. Таким образом, вам не нужно использовать набор пониманий, чтобы выразить эти идеи. Вместо этого вы могли бы просто сказать, A * B а также A + B соответственно.

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

Дафни использует синтаксическую эвристику, чтобы определить, является ли понимание множества конечным. К сожалению, эти эвристики нигде не документированы. Для целей этого вопроса ключевым моментом является то, что эвристика либо зависит от типа связанных переменных понимания, либо ищет конъюнкт, который ограничивает элементы, которые должны быть ограничены каким-либо другим способом. Например, Дафни может доказать

set x: int | 0 <= x < 10 && ...

конечно, а также

set x:A | x in S && ...

В обоих случаях важно, чтобы соответствующие границы были соединены. У Дафни нет синтаксической эвристики для доказательства ограничения на дизъюнкцию, хотя можно было бы добавить ее. Вот почему Дафни не может доказать вашу union функция конечная.

Кроме того, другой обходной путь будет использовать потенциально бесконечные множества (написано iset в Дафни). Если вам не нужно использовать количество наборов, то они могут работать лучше.