Блог

Я впервые задаю вопрос здесь, поэтому я надеюсь, что я должным образом следовал рекомендациям по заданию правильного вопроса.

Для краткого контекста: в настоящее время я пытаюсь реализовать и проверить рекурсивную версию Quicksort в Dafny. На данный момент кажется, что все, что осталось сделать, это доказать одну последнюю лемму (т. Е. Реализация полностью проверяется, когда я удаляю тело этой леммы. Если я не ошибаюсь, это должно означать, что реализация полностью проверяется при предположении, что эта лемма выполняется.).

В частности, эта лемма утверждает, что, если последовательность значений в настоящее время правильно разделена вокруг оси, то, если переставить (под) последовательности слева и справа от оси, полная последовательность по-прежнему является допустимым разделением. В конце концов, используя эту лемму, я, по сути, хочу сказать, что, если сортируются подпоследовательности слева и справа от pivot, полная последовательность по-прежнему является допустимым разделением; в результате сортируется полная последовательность.

Теперь я попытался доказать эту лемму, но я застрял на той части, где я пытаюсь показать, что если все значения в последовательности меньше некоторого значения, то все значения в перестановке этой последовательности также меньше этого значения. Конечно, мне также нужно показать эквивалентное свойство с заменой «меньше» на «больше или равно», но я полагаю, что они почти идентичны, поэтому достаточно знать одно.

Соответствующая часть кода приведена ниже:

 predicate Permutation(a: seq<int>, b: seq<int>)
    requires 0 <= |a| == |b|
{
    multiset(a) == multiset(b)
}

predicate Partitioned(a: seq<int>, lo: int, hi: int, pivotIndex: int)
    requires 0 <= lo <= pivotIndex < hi <= |a|
{
    (forall k :: lo <= k < pivotIndex ==> a[k] < a[pivotIndex])
    amp;amp;
    (forall k :: pivotIndex <= k < hi ==> a[k] >= a[pivotIndex])
}

lemma PermutationPreservesPartition(apre: seq<int>, apost: seq<int>, lo: int, hi: int, pivotIndex: int)
    requires 0 <= lo <= pivotIndex < hi <= |apre| == |apost|
    requires Partitioned(apre, lo, hi, pivotIndex)
    requires Permutation(apre[lo..pivotIndex], apost[lo..pivotIndex])
    requires Permutation(apre[pivotIndex   1..hi], apost[pivotIndex   1..hi])
    requires apre[pivotIndex] == apost[pivotIndex]

    ensures Partitioned(apost, lo, hi, pivotIndex)
{

}
 

Я пробовал несколько вещей, таких как:

 assert
Partitioned(apre, lo, hi, pivotIndex) amp;amp; apre[pivotIndex] == apost[pivotIndex]
==>
(
    (forall k :: lo <= k < pivotIndex ==> apre[k] < apost[pivotIndex])
    amp;amp;
    (forall k :: pivotIndex <= k < hi ==> apre[k] >= apost[pivotIndex])
);

assert
(forall k :: lo <= k < pivotIndex ==> apre[k] < apost[pivotIndex])
amp;amp;
(Permutation(apre[lo..pivotIndex], apost[lo..pivotIndex]))
==>
(forall k :: lo <= k < pivotIndex ==> apost[k] < apost[pivotIndex]);
 

Однако здесь второе утверждение уже не проверяется.

После этой первой попытки я подумал, что Dafny, возможно, не сможет проверить это свойство между последовательностями, потому что предикат «Перестановки» использует соответствующие мультимножества вместо самих последовательностей. Итак, я попытался сделать связь между последовательностями более явной, выполнив следующее:

 assert 
Permutation(apre[lo..pivotIndex], apost[lo..pivotIndex])
==>
forall v :: v in multiset(apre[lo..pivotIndex]) <==> v in multiset(apost[lo..pivotIndex]);

assert
forall v :: v in multiset(apre[lo..pivotIndex]) <==> v in apre[lo..pivotIndex];

assert
forall v :: v in multiset(apost[lo..pivotIndex]) <==> v in apost[lo..pivotIndex];

assert
forall v :: v in apre[lo..pivotIndex] <==> v in apost[lo..pivotIndex];

assert
(
    (forall v :: v in apre[lo..pivotIndex] <==> v in apost[lo..pivotIndex]) 
    amp;amp;
    (forall v :: v in apre[lo..pivotIndex] ==> v < apre[pivotIndex])
)
==>
(forall v :: v in apost[lo..pivotIndex] ==> v < apre[pivotIndex]);

assert
(
    (forall v :: v in apost[lo..pivotIndex] ==> v < apre[pivotIndex])
    amp;amp;
    apre[pivotIndex] == apost[pivotIndex]
)
==>
(forall v :: v in apost[lo..pivotIndex] ==> v < apost[pivotIndex]);
 

Все это проверяется, что, на мой взгляд, было здорово, поскольку, похоже, остался только один шаг, чтобы связать это с определением «Разделенный», а именно.:

 assert
(forall v :: v in apost[lo..pivotIndex] ==> v < apost[pivotIndex])
==>
(forall k :: lo <= k < pivotIndex ==> apost[k] < apost[pivotIndex]);
 

Тем не менее, Dafny не может проверить это утверждение.

Итак, на данный момент я не уверен, как убедить Dafny в том, что эта лемма справедлива. Я пытался посмотреть реализации быстрой сортировки в Dafny от других людей, а также любой потенциально релевантный вопрос, который я мог найти. Однако это пока безрезультатно. Я надеюсь, что кто-нибудь может мне здесь помочь.

Мои извинения за любое потенциальное невежество в отношении Dafny, я только начинаю с языка.

Трудно дать применимое определение «перестановки». Однако, чтобы доказать правильность алгоритма сортировки, вам нужно только, чтобы мультимножество элементов оставалось неизменным. Для последовательности s выражение multiset(s) дает вам мультимножество элементов s . Если вы начинаете с массива a , то a[..] выдает вам последовательность, состоящую из элементов массива, поэтому multiset(a[..]) дает вам мультимножество элементов в массиве.

См https://github.com/dafny-lang/dafny/blob/master/Test/dafny3/GenericSort.dfy#L59 для примера.

Верификатор Dafny не может самостоятельно обрабатывать все свойства таких мультимножеств. Однако, как правило, понятно, что мультимножество элементов остается неизменным при замене двух элементов.