Вот один из способов сделать это.
Ключ состоит в том, чтобы ввести понятие «набор индексов, которые еще не были окрашены в ложь». Для этой концепции я использую функцию TrueIndices.
function TrueIndices(a: array<bool>): set<int>
reads a
{
set i | 0 <= i < a.Length && a[i]
}
Начало метода BFS остается неизменным:
method BFS(G : Graph, s : int) returns (d : array<int>)
requires 0 <= s < |G.adjList|
requires forall u :: 0 <= u < |G.adjList| ==>
forall v :: 0 <= v < |G.adjList[u]| ==> 0 <= G.adjList[u][v] < |G.adjList|
requires forall u :: 0 <= u < |G.adjList| ==>
forall v,w :: 0 <= v < w < |G.adjList[u]| ==> G.adjList[u][v] != G.adjList[u][w]
{
var i := 0;
var j := 0;
var u : int;
var Q : seq<int>;
var iterations := G.adjList[0];
var n := |G.adjList|;
var color : array<bool>;
color := new bool[n];
d := new int [n];
i := 0; while (i < n)
{
color[i] := true;
d[i] := -1;
i := i + 1;
}
В реализации используется рабочий список Q. В этом случае алгоритм открывает элемент рабочего списка, а затем отмечает всех непосещенных соседей как посещенных. Если непосещенных соседей нет, то размер рабочего списка уменьшается. Если есть непосещенные соседи, они помечаются как посещенные, поэтому общее количество непосещенных узлов уменьшается. количество непосещенных узлов остается прежним, но длина рабочего списка уменьшается. Мы можем формализовать это рассуждение, сказав, что l oop уменьшает кортеж (number of unvisited nodes, length of Q) в лексикографическом порядке c.
Это именно то, что закодировано в предложении уменьшения ниже.
Q := [s];
while (Q != [])
decreases TrueIndices(color), |Q|
invariant forall x | x in Q :: 0 <= x < |G.adjList| // invariant (1)
{
ghost var top_of_loop_indices := TrueIndices(color);
ghost var top_of_loop_Q := Q;
// u <- Dequeue(Q)
u := Q[0]; Q := Q[1..];
assert u in top_of_loop_Q; // trigger invariant (1) for u
// help Dafny see that dequeueing is ok
assert forall x | x in Q :: x in top_of_loop_Q;
// foreach v in adjList[u]
i := 0; while i < |G.adjList[u]|
invariant forall x | x in Q :: 0 <= x < |G.adjList| // invariant (2)
invariant // invariant (3)
|| TrueIndices(color) < top_of_loop_indices
|| (TrueIndices(color) == top_of_loop_indices && |Q| < |top_of_loop_Q|)
{
var v := G.adjList[u][i];
if (color[v])
{
// help Dafny see that v was newly colored false
assert v in TrueIndices(color);
color[v] := false;
d[v] := d[u] + 1;
Q := Q + [v];
}
i := i + 1;
}
}
}
Код также содержит несколько инвариантов и утверждений, необходимых для доказательства предложения уменьшения. Вы можете остановиться на этом этапе и попытаться выяснить их самостоятельно, начиная только с пункта об уменьшении. Или вы можете прочитать повествование ниже, чтобы увидеть, как я это понял.
Если вы просто добавите условие уменьшения, вы получите две ошибки. Во-первых, Дафни скажет, что не может доказать, что статья об уменьшении уменьшается. Вернемся к этому. Вторая ошибка - это ошибка «индекс вне допустимого диапазона» для выражения G.adjList[u] в условии l oop внутреннего l oop. По сути, он не может доказать, что u здесь находится в границах. Что имеет смысл, потому что u - это просто произвольный элемент из Q, и мы еще не указали никаких l oop инвариантов около Q.
Чтобы исправить это, нам нужно чтобы сказать, что каждый элемент Q является допустимым индексом в G.adjList. Об этом свидетельствует строка, помеченная выше // invariant (1).
К сожалению, добавление только этой строки не сразу решает проблему. И мы получаем дополнительную ошибку, что новый инвариант l oop, который мы только что добавили, может не поддерживаться l oop. Почему этот инвариант не исправил ошибку? Проблема в том, что для Дафни все еще не очевидно, что u является элементом Q, хотя u определено как Q[0]. Мы можем исправить это, добавив утверждение с пометкой // trigger invariant (1) for u.
Теперь давайте попробуем доказать, что invariant (1) сохраняется l oop. Проблема в том, что существует внутренний l oop без инвариантов l oop. Итак, Дафни делает предположения наихудшего случая о том, что внутренний l oop может сделать с Q. Мы можем исправить это, скопировав тот же инвариант во внутренний l oop, который я пометил как // invariant (2) выше.
Это исправляет внешний l oop, может не сохранить invariant (1) "ошибка, но теперь мы получаем новую ошибку, говорящую, что invariant (2) может не удерживать вход во внутренний l oop. Что дает? Все, что мы сделали с момента начала внешнего l oop, - это удалить из очереди элемент Q. Мы можем помочь Дафни увидеть, что все элементы после удаления из очереди также были элементами исходного Q в верхней части l oop. Мы делаем это, используя утверждение, отмеченное // help Dafny see that dequeueing is ok выше.
Хорошо, это завершает доказательство invariant (1). Теперь давайте исправим оставшуюся ошибку, сказав, что условие уменьшения может не уменьшаться.
Опять же, проблема заключается во внутреннем l oop. В отсутствие инвариантов Дафни делает наихудшие предположения о том, что может случиться с color и Q. По сути, нам нужно найти способ гарантировать, что после завершения внутреннего l oop кортеж (TrueIndices(color), |Q|) лексикографически уменьшился по сравнению с его значением в верхней части внешнего l oop. Мы делаем это, разъясняя, что означает здесь lexicographi c ordering: либо TrueIndices(color) становится строго меньше, либо остается неизменным, а |Q| становится меньше. Это указано как // invariant (3) выше. (Обратите внимание, что, к сожалению, упорядочение кортежей (a, b) < (c, d), похоже, здесь не работает. Я заглянул под обложку, и то, что он на самом деле делает, довольно странно. Не совсем уверен, почему это так, но пусть будет так . Я подал вопрос об этом здесь .)
Добавление invariant (3) вызывает ошибку о том, что предложение уменьшения не уменьшается до go, но мы получаем одну последнюю ошибку, которая является что invariant (3) может не сохраняться внутренним l oop. Проблема здесь в основном в том, что внутри истинной ветви if нам нужно помочь Дафни понять, что v - это индекс, который будет удален из TrueIndices, мы делаем это с утверждением, отмеченным // help Dafny see that v was newly colored false.
Это завершает доказательство завершения!
Обратите внимание, что, как это часто бывает в сложных аргументах завершения, нам пришлось доказать несколько других инвариантов на этом пути. Сначала это может показаться вам несколько неожиданным, поскольку может показаться, что завершение и правильность не зависят друг от друга. Но на самом деле это довольно распространенное явление.
Конечно, для фактического доказательства функциональной корректности BFS потребуется еще больше инвариантов. Я не пробовал, но надеюсь, что вы попробуете!