Там нет никаких теоретических трудностей, просто вопрос добавления реализации. В самом деле, если выражение было сначала преобразовано в дизъюнкцию, то текущая эвристика может выполняться для каждого дизъюнкта, а затем результаты могут быть объединены. Реализация уже настроена для работы с различными видами «ограниченных пулов», поэтому добавление всеобъемлющего «ограниченного пула дизъюнкции» подойдет. (Это был бы отличный студенческий проект. :))
ни нет проблем с этим определением функции пересечения множеств.
function method intersection(A: set<int>, B: set<int>): (r: set<int>)
{
set x | x in A && x in B
}
Но когда дело доходит до объединения, Дафни жалуется, «понимание набора должно производить конечный набор, но эвристика Дафни не может понять, как создать ограниченный набор значений для« x »». A и B конечны, и поэтому, очевидно, объединение тоже.
function method union(A: set<int>, B: set<int>): (r: set<int>)
{
set x | x in A || x in B
}
Чем объясняется это, на первый взгляд, несоответствующее поведение?