"как развлечь себя во время секса"
Dec. 2nd, 2015 02:10 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonКогда-то давно узнал о языке и верификаторе Dafny, но пощупать не решался. А недавно таки собрался, поставил и поигрался. Довольно занятная вещь, я уже вижу где можно попытаться применить ее в работе.
Цитата из википедии: "Миф о Дафне, превратившейся в лавр, зародился в эпоху эллинизма[17]. По некоторому мнению, ему не следует придавать особого значения, поскольку, как считает И. И. Маханьков, он явно позднейшего происхождения и создан с целью объяснить особую роль лавра в культе Аполлона". А, не, не то.
Dafny - это язык программирования, похожий на упрощенный C#/Java/whatever с рядом дополнительных фишек. Там классы (в том числе генерики), объекты, у них поля, методы с императивным кодом, в них переменные, циклы, мутабельные массивы и прочие радости императивного программирования. К этому добавлены индуктивные и коиндуктивные алгебраические типы и паттерн-матчинг по ним. Компилятор из этого генерит C# и из него уже рабочие бинарники, которые можно позапускать. А дальше начинается интересное. В язык включены конструкции для указания пред- и пост-условий методов, ассертов в коде, а также инвариантов циклов и метрик завершимости, причем записываются весьма удобным и человечным языком. И вторая часть компилятора - это верификатор, который все эти условия проверяет статически. Для этого он внутри генерит спецификации на Boogie, который в свою очередь использует SMT-солвер Z3. SMT, как известно, это Sick Magic Trickery, поэтому возможности верификатора к пониманию кода и самостоятельным выводам весьма впечатляют. Это вам не коммутативность сложения доказывать в четырехсотый раз. В результате программы на Dafny как минимум доказанно не вылетают за границы массивов (и вообще никуда не вылетают) и всегда завершаются, а как норма - еще и доказанно делают то, что должны.
Язык различает императивные методы (method), для которых указывается, что они меняют, и математически чистые функции (function), для которых указывается, что они читают. Такие функции обычно вызываются из разных предикатов, т.е. относятся к верификационной части, и по умолчанию исполняемый код из них не генерится (все ассерты, пред/постусловия и инварианты делают свое дело во время компиляции и в исполняемый код не попадают, полностью стираются). Но если нужно такую чистую функцию использовать в рантайме, то это тоже можно, просто надо назвать ее function method. Еще можно добавлять фиктивные переменные и методы, дописав перед ними слово ghost. В коде ими можно манипулировать как с обычными переменными, хранить там всякие нужные для описания инвариантов вещи и использовать их в спецификациях, а при компиляции они тоже будут полностью стерты, и в рантайме их не будет.
Сперва пример из учебника. Хотим сделать бинарный поиск в отсортированном массиве интов. Вот так можно определить отсортированность массива:
predicate означает чистую функцию, возвращающую bool. Неравенства можно, как тут, объединять в цепочки. "==>" это не особая синтаксическая фишка, а просто бинарный оператор импликации, работающий с bool'ами и имеющий низкий приоритет. Итак, тут говорится, что массив считается отсортированным, если для любых двух элементов тот, что левее, меньше или равен того, что правее.
Теперь сам метод бинарного поиска:
Предусловия записываются после слова requires, постусловия - после ensures. Тут мы говорим, что переданный на вход массив должен не быть null'ом и быть отсортированным (используется описанный выше предикат). Возвращаем индекс i, целое число, и обещаем в постусловии, что если это i неотрицательно, то оно меньше длины массива, т.е. валидный индекс, и по этому индексу в массиве находится искомое значение. А если вернем i меньше 0, то это значит, что во всем массиве искомого значения нет, все-все элементы отличаются от искомого key. Везде, где этот метод будет вызываться, верификатор должен будет убедиться статически, что предусловие выполнено (иначе - ошибка компиляции), и будет знать, что после вызова метода верны предикаты, указанные в постусловиях. Секрет успеха в том, что верификация идет по одному методу за раз: когда мы откуда-то вызываем этот binarySearch, на тело метода верификатор уже не смотрит, повторно не анализирует, ему видны только пред- и постусловия. Аналогично с циклами - ему не нужно крутить никакие циклы вообще, он смотрит лишь на их инварианты. Все это позволяет верификатору быть достаточно быстрым (какой-нибудь Идрис дольше тайпчекает).
Внутри метода мы определяем парочку переменных - границы поиска, изначально равные границам массива. Дальше в цикле мы смотрим на элемент между ними и сдвигаем их друг к другу, пока не найдем нужное значение или не сдвинем слишком близко. Ключевой инвариант цикла заключается в том, что за пределами интервала low..high искомого значения в массиве точно нет. Исходно этот интервал охватывает весь массив, за его пределами ничего нет. Потом, если например значение посередке a[mid] оказалось меньше искомого, то все элементы левее a[mid] тоже меньше - это следует из отсортированности массива, из sorted(a). А значит, можно переместить левую границу поиска до mid + 1: все предшестующие элементы меньше искомого. Аналогично с правой границей. В итоге после каждой итерации цикла (и перед первой) инвариант выполнен. Что происходит после цикла? Если мы из него вышли, значит условие цикла (low < high) больше не выполнено, а оба инварианта все еще в силе. Значит, low == high, и множество позиций за пределами интервала - это весь массив. Согласно инварианту теперь, во всем массиве нет искомого элемента. Пишем i := -1 и дело сделано, верификатор проверил, что код действительно делает верными постусловия при истинности предусловий, и теперь в вызывающем коде может забыть про внутренности binarySearch и полагаться на его пред/постусловия.
Я пробовал этот код пошевелить в разные стороны. Если вычислять mid как low + (high - low) / 3, например, код остается валидным и успешно верифицируется. А если (high + low) / 3, уже ругается - не уверен в завершимости цикла и в исполнении первого инварианта. Если неаккуратно high и low менять в цикле - не там единичку добавить или убавить, тоже ловит, ругается.
Да, все циклы и рекурсивные функции должны доказанно завершаться, причем обычно компилятор сам угадывает как себя в этом убедить - какое ограниченное снизу выражение с каждой итерацией уменьшается, а в некоторых случаях такое выражение ему надо подсказать словом decreases.
Поигравшись с примером из учебника, мне захотелось сделать что-то самостоятельно, и вот что вышло. Опишем примитивный метод сортировки, который превратит переданный массив интов в отсортированный согласно тому же предикату sorted, чтоб можно было в binarySearch использовать. Сначала написал просто код, как на обычном ЯП. Компилятор первым делом сказал, что я забыл на null проверить, и что метод должен задекларировать, что он полученный массив мутирует. Пришлось добавить пару строк:
Цикла for почему-то нет (наверное, неудобно предикаты вставлять), приходится делать while'ами. Алгоритм - самый простой пришедший на ум, вариант selection sort'a.
Теперь надо было добавить пред- и постусловия да инварианты, чтобы верификатор подтвердил, что на выходе массив отсортирован - ensures sorted(a). При этом сам код измениться не должен. Это вам не агда с идрисом, где чтобы какое-то свойство доказать, надо все заново переписать трижды.
Итак, у нас тут два цикла. Во внешнем цикле переменная i проходит по всем позициям массива кроме последней. Во внутреннем цикле переменная j пробегает по всем позициям правее i. После завершения внутреннего цикла с перестановками справа от a[i] нет элементов меньше оного, а элементы слева от a[i] уже не меняются. А значит, каждый следующий a[i] получается не меньше предыдущего (a[i-1]). Осталось отразить это в инвариантах и показать, что из такого попарного отношения между a[i] и a[i-1] следует отсортированность как ее понимает sorted(a). Долго ли, коротко ли (несколько часов, на самом деле), получилось вот как.
Свойство массива, что первые n элементов в нем так упорядочены - a[i-1] <= a[i]:
Но наш предикат sorted понимает отсортированность как подобное отношение между любыми элементами, не только соседними, и относится ко всему массиву целиком. Опишем его вариант для первых n элементов:
Теперь надо убедить верификатор, что это одно и то же, что из первого следует второе. Для этого нам пригодится lemma - это ghost method, т.е. не попадающий в рантайм метод, вся польза которого заключается в его пред- и пост-условиях: если он компилируется, значит из его предусловий следуют постусловия, т.е. он доказывает импликацию. Он должен показать, что если выполнено pairwiseOrdered(a, n), то для любых 0 <= i < j < n выполнено a[i] <= a[j].
Тут используется другая лемма, которая доказывает сей факт для конкретных i и j:
Если i и j соседи, то нужное условие уже выполнено, а если между ними есть другие элементы, то надо рекурсивно обратить свой взор на (i+1)-й элемент. Ежели мы докажем, что a[i+1] <= a[j], и раз мы знаем, что a[i] <= a[i+1], то требуемое отношение a[i] <= a[j] уже очевидно. Записывать так подробно не нужно - SMT солвер все это видит сам. Рекурсия обязана завершаться, и выражение "decreases j - i" помогает компилятору понять, почему она завершится.
Ну вот, имея эти леммы, можно уже получить конечный результат:
Вуаля! Массив отсортирован, потому что sorted(a) это sortedPart(a, a.Length) (это верификатор сам понимает), а sortedPart(a, a.Length) нам дает pairwiseOrderedIsSorted(a, a.Length), которая справедлива, потому что инвариант внешнего цикла дает pairwiseOrdered(a, i+1) для i > 0, а после цикла i = a.Length-1, т.е. имеем pairwiseOrdered(a, a.Length). А чтобы доказать, что pairwiseOrdered(a, i+1) справедлив в инварианте внешнего цикла, понадобились все остальные показанные тут условия и инварианты. Непосредственно код, который останется работать в рантайме, не изменился нисколько. Как я понял, какие именно инварианты нужно зафиксировать.. Ну, не сразу, долго и мучительно, нащупывая вставкой assert'ами разных условий и проверяя, какие из них верификатору ясны и видны, а какие нужно расписать явно. Основной принцип - если в цикле что-то делается с массивом, то после цикла верификатор почти ничего об этом массиве не знает кроме того, что сказано в инвариантах. Соответственно, нужен такой инвариант, который с одной стороны опишет результат всего цикла, а с другой стороны будет верен и до его завершения, и даже до начала.
На закуску - немного индуктивных и коиндуктивных типов.
В общем, крутотень. Одно лишь плохо: SMT это страшная магея, поэтому когда верификатор не может что-то доказать, он лишь говорит что именно он не смог доказать, а в качестве подробностей изрыгает мистическую трассу из потаенных уголков солвера, нифига не понятно. Тем не менее, проведя с ним вечер, начинаешь уже чуять, что он поймет, а где нужны разъяснения.
Цитата из википедии: "Миф о Дафне, превратившейся в лавр, зародился в эпоху эллинизма[17]. По некоторому мнению, ему не следует придавать особого значения, поскольку, как считает И. И. Маханьков, он явно позднейшего происхождения и создан с целью объяснить особую роль лавра в культе Аполлона". А, не, не то.
Dafny - это язык программирования, похожий на упрощенный C#/Java/whatever с рядом дополнительных фишек. Там классы (в том числе генерики), объекты, у них поля, методы с императивным кодом, в них переменные, циклы, мутабельные массивы и прочие радости императивного программирования. К этому добавлены индуктивные и коиндуктивные алгебраические типы и паттерн-матчинг по ним. Компилятор из этого генерит C# и из него уже рабочие бинарники, которые можно позапускать. А дальше начинается интересное. В язык включены конструкции для указания пред- и пост-условий методов, ассертов в коде, а также инвариантов циклов и метрик завершимости, причем записываются весьма удобным и человечным языком. И вторая часть компилятора - это верификатор, который все эти условия проверяет статически. Для этого он внутри генерит спецификации на Boogie, который в свою очередь использует SMT-солвер Z3. SMT, как известно, это Sick Magic Trickery, поэтому возможности верификатора к пониманию кода и самостоятельным выводам весьма впечатляют. Это вам не коммутативность сложения доказывать в четырехсотый раз. В результате программы на Dafny как минимум доказанно не вылетают за границы массивов (и вообще никуда не вылетают) и всегда завершаются, а как норма - еще и доказанно делают то, что должны.
Язык различает императивные методы (method), для которых указывается, что они меняют, и математически чистые функции (function), для которых указывается, что они читают. Такие функции обычно вызываются из разных предикатов, т.е. относятся к верификационной части, и по умолчанию исполняемый код из них не генерится (все ассерты, пред/постусловия и инварианты делают свое дело во время компиляции и в исполняемый код не попадают, полностью стираются). Но если нужно такую чистую функцию использовать в рантайме, то это тоже можно, просто надо назвать ее function method. Еще можно добавлять фиктивные переменные и методы, дописав перед ними слово ghost. В коде ими можно манипулировать как с обычными переменными, хранить там всякие нужные для описания инвариантов вещи и использовать их в спецификациях, а при компиляции они тоже будут полностью стерты, и в рантайме их не будет.
Сперва пример из учебника. Хотим сделать бинарный поиск в отсортированном массиве интов. Вот так можно определить отсортированность массива:
predicate sorted(a: array<int>)
requires a != null;
reads a;
{
forall j,k :: 0 <= j < k < a.Length ==> a[j] <= a[k]
}
predicate означает чистую функцию, возвращающую bool. Неравенства можно, как тут, объединять в цепочки. "==>" это не особая синтаксическая фишка, а просто бинарный оператор импликации, работающий с bool'ами и имеющий низкий приоритет. Итак, тут говорится, что массив считается отсортированным, если для любых двух элементов тот, что левее, меньше или равен того, что правее.
Теперь сам метод бинарного поиска:
method binarySearch(a : array<int>, key : int) returns (i : int)
requires a != null && sorted(a);
ensures 0 <= i ==> i < a.Length && a[i]==key;
ensures i < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key;
{
var low, high := 0, a.Length;
while(low < high)
invariant 0 <= low <= high <= a.Length;
invariant forall j :: 0 <= j < a.Length && !(low <= j < high) ==> a[j] != key;
{
var mid := (high + low) / 2;
if (a[mid] < key) {
low := mid + 1;
} else if (key < a[mid]) {
high := mid;
} else {
i := mid; return;
}
}
i := -1;
}
Предусловия записываются после слова requires, постусловия - после ensures. Тут мы говорим, что переданный на вход массив должен не быть null'ом и быть отсортированным (используется описанный выше предикат). Возвращаем индекс i, целое число, и обещаем в постусловии, что если это i неотрицательно, то оно меньше длины массива, т.е. валидный индекс, и по этому индексу в массиве находится искомое значение. А если вернем i меньше 0, то это значит, что во всем массиве искомого значения нет, все-все элементы отличаются от искомого key. Везде, где этот метод будет вызываться, верификатор должен будет убедиться статически, что предусловие выполнено (иначе - ошибка компиляции), и будет знать, что после вызова метода верны предикаты, указанные в постусловиях. Секрет успеха в том, что верификация идет по одному методу за раз: когда мы откуда-то вызываем этот binarySearch, на тело метода верификатор уже не смотрит, повторно не анализирует, ему видны только пред- и постусловия. Аналогично с циклами - ему не нужно крутить никакие циклы вообще, он смотрит лишь на их инварианты. Все это позволяет верификатору быть достаточно быстрым (какой-нибудь Идрис дольше тайпчекает).
Внутри метода мы определяем парочку переменных - границы поиска, изначально равные границам массива. Дальше в цикле мы смотрим на элемент между ними и сдвигаем их друг к другу, пока не найдем нужное значение или не сдвинем слишком близко. Ключевой инвариант цикла заключается в том, что за пределами интервала low..high искомого значения в массиве точно нет. Исходно этот интервал охватывает весь массив, за его пределами ничего нет. Потом, если например значение посередке a[mid] оказалось меньше искомого, то все элементы левее a[mid] тоже меньше - это следует из отсортированности массива, из sorted(a). А значит, можно переместить левую границу поиска до mid + 1: все предшестующие элементы меньше искомого. Аналогично с правой границей. В итоге после каждой итерации цикла (и перед первой) инвариант выполнен. Что происходит после цикла? Если мы из него вышли, значит условие цикла (low < high) больше не выполнено, а оба инварианта все еще в силе. Значит, low == high, и множество позиций за пределами интервала - это весь массив. Согласно инварианту теперь, во всем массиве нет искомого элемента. Пишем i := -1 и дело сделано, верификатор проверил, что код действительно делает верными постусловия при истинности предусловий, и теперь в вызывающем коде может забыть про внутренности binarySearch и полагаться на его пред/постусловия.
Я пробовал этот код пошевелить в разные стороны. Если вычислять mid как low + (high - low) / 3, например, код остается валидным и успешно верифицируется. А если (high + low) / 3, уже ругается - не уверен в завершимости цикла и в исполнении первого инварианта. Если неаккуратно high и low менять в цикле - не там единичку добавить или убавить, тоже ловит, ругается.
Да, все циклы и рекурсивные функции должны доказанно завершаться, причем обычно компилятор сам угадывает как себя в этом убедить - какое ограниченное снизу выражение с каждой итерацией уменьшается, а в некоторых случаях такое выражение ему надо подсказать словом decreases.
Поигравшись с примером из учебника, мне захотелось сделать что-то самостоятельно, и вот что вышло. Опишем примитивный метод сортировки, который превратит переданный массив интов в отсортированный согласно тому же предикату sorted, чтоб можно было в binarySearch использовать. Сначала написал просто код, как на обычном ЯП. Компилятор первым делом сказал, что я забыл на null проверить, и что метод должен задекларировать, что он полученный массив мутирует. Пришлось добавить пару строк:
method sort(a : array<int>)
requires a != null;
modifies a;
{
var i := 0;
while (i < a.Length-1)
{
var j := i + 1;
while (j < a.Length)
{
if (a[i] > a[j]) {
a[i], a[j] := a[j], a[i];
}
j := j+1;
}
i := i+1;
}
}
Цикла for почему-то нет (наверное, неудобно предикаты вставлять), приходится делать while'ами. Алгоритм - самый простой пришедший на ум, вариант selection sort'a.
Теперь надо было добавить пред- и постусловия да инварианты, чтобы верификатор подтвердил, что на выходе массив отсортирован - ensures sorted(a). При этом сам код измениться не должен. Это вам не агда с идрисом, где чтобы какое-то свойство доказать, надо все заново переписать трижды.
Итак, у нас тут два цикла. Во внешнем цикле переменная i проходит по всем позициям массива кроме последней. Во внутреннем цикле переменная j пробегает по всем позициям правее i. После завершения внутреннего цикла с перестановками справа от a[i] нет элементов меньше оного, а элементы слева от a[i] уже не меняются. А значит, каждый следующий a[i] получается не меньше предыдущего (a[i-1]). Осталось отразить это в инвариантах и показать, что из такого попарного отношения между a[i] и a[i-1] следует отсортированность как ее понимает sorted(a). Долго ли, коротко ли (несколько часов, на самом деле), получилось вот как.
Свойство массива, что первые n элементов в нем так упорядочены - a[i-1] <= a[i]:
predicate pairwiseOrdered(a : array, n : int) requires a != null; requires n <= a.Length; reads a; { forall i :: 0 <= i < n-1 ==> a[i] <= a[i+1] }
Но наш предикат sorted понимает отсортированность как подобное отношение между любыми элементами, не только соседними, и относится ко всему массиву целиком. Опишем его вариант для первых n элементов:
predicate sortedPart(a: array, n : int) requires a != null; requires n <= a.Length; reads a; { forall j,k :: 0 <= j < k < n ==> a[j] <= a[k] }
Теперь надо убедить верификатор, что это одно и то же, что из первого следует второе. Для этого нам пригодится lemma - это ghost method, т.е. не попадающий в рантайм метод, вся польза которого заключается в его пред- и пост-условиях: если он компилируется, значит из его предусловий следуют постусловия, т.е. он доказывает импликацию. Он должен показать, что если выполнено pairwiseOrdered(a, n), то для любых 0 <= i < j < n выполнено a[i] <= a[j].
lemma pairwiseOrderedIsSorted(a : array<int>, n : int)
requires a != null;
requires n <= a.Length;
requires pairwiseOrdered(a, n);
ensures sortedPart(a, n);
{
forall(i, j | 0 <= i < j < n) { transitivelyOrdered(a, n, i, j); }
}
Тут используется другая лемма, которая доказывает сей факт для конкретных i и j:
lemma transitivelyOrdered(a: array, n : int, i : int, j : int) requires a != null; requires n <= a.Length; requires forall i :: 0 <= i < n-1 ==> a[i] <= a[i+1]; requires 0 <= i < j < n; decreases j - i; ensures a[i] <= a[j]; { if (j == i + 1) { } else { transitivelyOrdered(a, n, i+1, j); } }
Если i и j соседи, то нужное условие уже выполнено, а если между ними есть другие элементы, то надо рекурсивно обратить свой взор на (i+1)-й элемент. Ежели мы докажем, что a[i+1] <= a[j], и раз мы знаем, что a[i] <= a[i+1], то требуемое отношение a[i] <= a[j] уже очевидно. Записывать так подробно не нужно - SMT солвер все это видит сам. Рекурсия обязана завершаться, и выражение "decreases j - i" помогает компилятору понять, почему она завершится.
Ну вот, имея эти леммы, можно уже получить конечный результат:
method sort(a : array<int>)
requires a != null;
requires a.Length >= 1;
modifies a;
ensures sorted(a); // ура!
{
var i := 0;
while (i < a.Length-1)
invariant i >= 0 && i < a.Length;
invariant 0 < i ==> pairwiseOrdered(a, i+1);
invariant forall e :: 0 < i < e < a.Length ==> a[i-1] <= a[e];
{
var j := i + 1;
while (j < a.Length)
invariant j <= a.Length;
invariant forall e :: 0 <= i < e < j <= a.Length ==> a[i] <= a[e];
invariant forall r :: 0 < i < r < a.Length ==> a[i-1] <= a[r];
invariant pairwiseOrdered(a, i+1);
{
if (a[i] > a[j]) {
a[i], a[j] := a[j], a[i];
}
j := j+1;
}
i := i+1;
}
pairwiseOrderedIsSorted(a, a.Length);
}
Вуаля! Массив отсортирован, потому что sorted(a) это sortedPart(a, a.Length) (это верификатор сам понимает), а sortedPart(a, a.Length) нам дает pairwiseOrderedIsSorted(a, a.Length), которая справедлива, потому что инвариант внешнего цикла дает pairwiseOrdered(a, i+1) для i > 0, а после цикла i = a.Length-1, т.е. имеем pairwiseOrdered(a, a.Length). А чтобы доказать, что pairwiseOrdered(a, i+1) справедлив в инварианте внешнего цикла, понадобились все остальные показанные тут условия и инварианты. Непосредственно код, который останется работать в рантайме, не изменился нисколько. Как я понял, какие именно инварианты нужно зафиксировать.. Ну, не сразу, долго и мучительно, нащупывая вставкой assert'ами разных условий и проверяя, какие из них верификатору ясны и видны, а какие нужно расписать явно. Основной принцип - если в цикле что-то делается с массивом, то после цикла верификатор почти ничего об этом массиве не знает кроме того, что сказано в инвариантах. Соответственно, нужен такой инвариант, который с одной стороны опишет результат всего цикла, а с другой стороны будет верен и до его завершения, и даже до начала.
На закуску - немного индуктивных и коиндуктивных типов.
datatype Tree<T> = Empty | Node(Tree<T>, T, Tree<T>) // алгебраик
function method size<T>(t : Tree<T>) : int
{
match t
case Empty => 0
case Node(l,x,r) => size(l) + 1 + size(r)
}
//бесконечный поток - коиндуктивный тип
codatatype IStream<T> = ICons(head : T, tail : IStream)
//поэлементное произведение, работает лениво
function method Mult(a : IStream<int>, b : IStream<int>): IStream<int>
{
ICons(a.head * b.head, Mult(a.tail, b.tail))
}
//копредикат - тут работает с бесконечными потоками, сравнивает лексикографически
copredicate Below(a : IStream<int>, b : IStream<int>)
{
a.head <= b.head && (a.head == b.head ==> Below(a.tail, b.tail))
}
// лемма о том, что x <= x*x, где x - поток интов
colemma BelowSquare(a : IStream<int>)
ensures Below(a, Mult(a,a));
{ } // proved automatically!
В общем, крутотень. Одно лишь плохо: SMT это страшная магея, поэтому когда верификатор не может что-то доказать, он лишь говорит что именно он не смог доказать, а в качестве подробностей изрыгает мистическую трассу из потаенных уголков солвера, нифига не понятно. Тем не менее, проведя с ним вечер, начинаешь уже чуять, что он поймет, а где нужны разъяснения.
Re: В дополнение
Date: 2015-12-04 04:47 pm (UTC)Re: В дополнение
Date: 2015-12-04 07:31 pm (UTC)