"как развлечь себя во время секса"

[thedeemon]

Когда-то давно узнал о языке и верификаторе Dafny, но пощупать не решался. А недавно таки собрался, поставил и поигрался. Довольно занятная вещь, я уже вижу где можно попытаться применить ее в работе.

Цитата из википедии: "Миф о Дафне, превратившейся в лавр, зародился в эпоху эллинизма[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 это страшная магея, поэтому когда верификатор не может что-то доказать, он лишь говорит что именно он не смог доказать, а в качестве подробностей изрыгает мистическую трассу из потаенных уголков солвера, нифига не понятно. Тем не менее, проведя с ним вечер, начинаешь уже чуять, что он поймет, а где нужны разъяснения.

Comments

[deni-ok.livejournal.com]

Мне в таких системах все нравится, за исключением одного: то, что верификатор не пропустит код с каким-то классом дырок, я должен принять на веру. Или сейчас сами SMT-солверы проходят полную формальную верификацию в более простых движках?

[thedeemon.livejournal.com]

Хороший вопрос. Не знаю.

[valentin budaev (from livejournal.com)]

Ну так это проблема принципиально неустранима. Если верифицировать смт-солвер чем-то, то можно спросить - а кто сказал что это что-то само по себе работает корректно?

[deni-ok.livejournal.com]

Мартин-Лёф.

[valentin budaev (from livejournal.com)]

Что "Мартин-Лёф"?

[thedeemon.livejournal.com]

-кто сказал, что ...?
-Мартин-Лёф сказал.

[valentin budaev (from livejournal.com)]

Аааа. Ну так тогда стоит ставить вопрос о том, кто верифицировал Мартина-Лёфа :)

[deni-ok.livejournal.com]

Ну у меня с этим строго: те студенты, которые Мартин-Лёфа верифицировать не могут, зачета не получают.

[valentin budaev (from livejournal.com)]

> Ну у меня с этим строго: те студенты, которые Мартин-Лёфа верифицировать не могут, зачета не получают.

Ага, значит, Мартина-Лёфа верифицируют студенты, вы верифицируете студентов, а вас кто верифицирует?

[sassa-nf.livejournal.com]

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

[stdray.livejournal.com]

Они сделали Code Contracts, F* и нечто среднее. Выглядит очень интересно, надо будет посмотреть.

[valentin budaev (from livejournal.com)]

О! Верификация без рака зависимых типов, почти как в моих влажных фантазиях! Спасибо автору.

Один момент только хотелось бы отметить:
> requires a != null;
> requires a.Length >= 1;
> modifies a;
> ensures sorted(a); // ура!

Если заполнить массив а нулями то ф-я пройдет тайпчек, то есть, как обычно, забыли условие на то, что результат является перестановкой оригинала. Как, кстати, фиксировать этот факт? По идее нужен какой-то предикат вроде permutation(a, b), только как это записать в ensures, ведь у нас там а и а, с-но надо как-то permutation(a_argument, a_result)?

[thedeemon.livejournal.com]

Да, этот момент я тут не доказывал, чтобы сильнее код не раздувать.
Вообще для этих целей есть две вещи: встроенные multisets и выражение old(...) в постусловиях. Выглядит так:

method test(a : array<int>)
  requires a != null && a.Length >= 2;
  modifies a;
  ensures isPerm(a, old(a));   // здеся
{
  a[0], a[1] := a[1], a[0];
}

Где isPerm я определил так:

predicate isPerm<T(==)>(a : array<T>, b : array<T>)
  requires a != null && b != null;
  reads a, b;
{
  elements(a) == elements(b)
}

function method multisetOf<T>(a : array<T>, i : int) : multiset<T>
  requires a != null;
  requires 0 <= i <= a.Length;
  reads a;
  decreases a.Length - i;
{
  if i == a.Length then multiset{}
  else multisetOf(a, i+1) + multiset{a[i]}
}

function method elements<T>(a : array<T>) : multiset<T>
  requires a != null;
  reads a;
{
  multisetOf(a,0)
}

т.е. можно в явном виде сказать в постусловии "набор (мультисет) элементов в массиве не изменился".

стоп, стоп...

[serge shikov (from livejournal.com)]

В результате программы на Dafny как минимум доказанно не вылетают за границы массивов (и вообще никуда не вылетают) и всегда завершаются, а как норма - еще и доказанно делают то, что должны.

Это часом не эквивалентно проблеме останова для машины Тьюринга, которая вроде неразрешима? А если нет, то почему?

RE: стоп, стоп...

[109.livejournal.com]

я не думаю, что в Dafny есть пост-условие ensures halting(in finite time) :)

а без этого инварианта даже доказанно правильно работающая программа не противоречит halting problem, если не гарантировано, что она закончится.

Re: стоп, стоп...

[thedeemon.livejournal.com]

Это условие там встроено - ВСЕ циклы и функции должны доказанно завершаться за конечное время. Если про какой-то цикл компилятор не будет в этом уверен - программу не примет.

Re: стоп, стоп...

[valentin budaev (from livejournal.com)]

А как ио, кстати, работает?

Re: стоп, стоп...

[thedeemon.livejournal.com]

Из IO там только print, он получает конечные данные и точно завершается. Другого IO там нет. :)

Re: стоп, стоп...

[serge shikov (from livejournal.com)]

Хорошо, IO нету (точнее только вывод), это уже сильное ограничение. С точки зрения полезности платформы для практики - кстати тоже.

А что насчет всех функций, которые недоступны компилятору для анализа? В смысле, результат раздельной компиляции - он что, кроме кода еще некоторые утверждения о коде содержит тоже? Или ее (компиляции раздельной) не бывает?

Re: стоп, стоп...

[thedeemon.livejournal.com]

Там есть система модулей, но про раздельную компиляцию я не в курсе.
В некотором смысле она вся раздельная - если функция А вызывает ф-ю Б, то когда анализируется А, внутренности Б компилятору "не видны", он полагается лишь на внешнюю спецификацию Б - тип и пред/постусловия.
Не скажу за Dafny, но в во многом похожей системе ATS для внешних функций (например, из C runtime) указывались типы и такие же внешние спецификации, и верификатор принимал их как аксиомы.
Можно считать, что пред/постусловия - это часть типа, они должны быть в "заголовочных файлах".

Re: стоп, стоп...

[thedeemon.livejournal.com]

расписал про доказанную завершимость чуть подробнее:
http://thedeemon.livejournal.com/107067.html?thread=1823547#t1823547

Re: стоп, стоп...

[valentin budaev (from livejournal.com)]

> Это часом не эквивалентно проблеме останова для машины Тьюринга, которая вроде неразрешима? А если нет, то почему?

Задача останова должна определять завершимость _точно_, если же ослабить это условие и разрешить называть незавершающимися некоторый класс завершающихся программ, то задача сразу становится разрешимой. Именно так и делает dafny - если компилятор сказал что программа завершается (вывел это) то она наверняка завершается, если же компилятор завершаемость вывести не смог (может вывода нет - то есть программа действительно виснет, а может вывод есть и просто компилятор его не нашел, неизвестно) - он программу отвергает и заставляет переписать так, чтобы вывод после переписывания был найден.

Re: стоп, стоп...

[thedeemon.livejournal.com]

Не эквивалентно, потому что это не машина Тьюринга.
В машине Тьюринга циклы и переходы могут быть любыми, и у нас нет никаких выразительных средств подсказать машине или себе, почему они завершатся. Поэтому для МТ есть проблема останова. Здесь же если верификатор сам не видит, что рекурсия или цикл точно остановятся, он не примет такую программу и попросит подсказать.
Тут нет goto. Есть цикл forall, где аргумент проходится по конечному набору значений. Он завершается, очевидно.
Остаются два способа зациклиться: цикл while и рекурсия. Если условие в while достаточно простое, как в примерах из поста, верификатор видит, что переменная цикла с каждой итерацией растет и приближается к своей границе из условия, тут он сам способен доказать завершимость. Если же там что-то менее ему очевидное, то он попросит в цикле указать ключевым словом decreases ограниченное снизу выражение, которое уменьшается на каждой итерации. Это гарантирует завершимость цикла. Аналогично с рекурсией. Если это структурная рекурсия, как в ф-ии size из поста, где в рекурсивных вызовах передаются части от полученного аргумента (хвост от списка или поддерево от дерева и т.п.), то этого достаточно для доказанности завершимости, т.к. подобные типы данных всегда конечны и с каждой итерацией там данных все меньше. Если в рекурсии что-то менее очевидное, то опять используется decreases. Вот, например, знаменитая функция Аккермана:

function Ackermann(m: int, n: int): int
  decreases m, n
{
  if m <= 0 then
    n + 1
  else if n <= 0 then
    Ackermann(m - 1, 1)
  else
    Ackermann(m - 1, Ackermann(m, n - 1))
}

Она гарантированно завершается, т.к. при каждом рекурсивном вызове мы или уменьшаем m, или оставляем m тем же, но уменьшаем n. Значит, пара (m,n) с каждым вызовом лексикографически меньше предыдущей. Ее указания верификатору достаточно, чтобы убедиться в завершимости.
Разумеется, тот факт, что указанные в decreases выражения с каждой итерацией уменьшаются, верификатор тоже проверяет, на слово не верит.

Re: стоп, стоп...

[swizard.livejournal.com]

> он попросит в цикле указать ключевым словом decreases ограниченное снизу выражение, которое уменьшается на каждой итерации. Это гарантирует завершимость цикла.

А как он проверит завершаемость этого цикла?

  var i := 1;
  var x := 1;
  while (x > 0)
  {
    x := x / i;
    i := i + 1;
  }

вроде оно и уменьшается, но до нуля не доходит

Re: стоп, стоп...

[thedeemon.livejournal.com]

Вот такая программа верифицируется без вопросов:

method Main()
{
  var i := 2; // тип выводится как int
  var x := 1;
  while (x > 0)
  {
    x := x / i;  // деление целочисленное!
    i := i + 1;
  }
  print i;
}

А вот если вначале i := 1, то x не на каждой итерации уменьшается. Как показать завершимость оригинального варианта, не разбивая цикл, пока не знаю.

эврика!

[thedeemon.livejournal.com]

method Main()
{
  var i := 1;
  var x := 1;
  while (x > 0)
    decreases x, 2-i;
  {
    x := x / i;
    i := i + 1;
  }
  print i;
}

Так все принимает.

Re: стоп, стоп...

[valentin budaev (from livejournal.com)]

> вроде оно и уменьшается, но до нуля не доходит

Дык это, если (бы оно до нуля не доходит то и завершимость очевидно доказать нельзя. Так как ее нет.

Если не про dafna

[parse error (from livejournal.com)]

Раз до нуля не доходит, значит, под типом переменной x подразумеваются конструктивные вещественные числа (потому что целые и плавающая точка таки доходят до ноля при достаточном количестве итераций деления.) А для таких чисел вы не докажете теорему индукции, которая доказывает завершимость, а ради этой теоремы, собственно, и нужно доказательство убывания агрументов.

Интересно, как это все будет выглядеть в Dafna.

Re: Если не про dafna

[thedeemon.livejournal.com]

В Dafny есть рациональные числа (бесконечной точности).
Но для них же этот код не завершается.

В дополнение

[parse error (from livejournal.com)]

Что интересно, можно, в принципе, написать программу, которая определяет завершимость для любой реальной программы. Потому что пространство реальных программ* ничтожно по сравнению с пространством всех программ и имеет дополнительную структуру.

* реальными программами назовем в точности все программы, которые когда-либо были или будут написаны человечеством для пользы дела, а не чтобы поиздеваться над автоматикой ;)

Re: В дополнение

[thedeemon.livejournal.com]

А сама эта программа будет завершаться за приемлемое время?

Или там просто "return true", т.к. каждый конкретный компьютер рано или поздно перестает работать? :)

Re: В дополнение

[parse error (from livejournal.com)]

Нет, всё честно.

С подвохами -- не интересно.

Re: В дополнение

[parse error (from livejournal.com)]

Еще интересно что, образно выражаясь, для 90% кода 90% программ это вполне возможно уже сейчас -- например, в коде PhpBB нет ни одного сложного цикла, только простые For со счетчиками и ForEach. (Ну, или если я случайно не пропустил)

Re: В дополнение

[zaharchenko]

Но такая программа не поможет от случайно сделанных ошибок которые приводят к незавершенности, а собственно именно такие и ошибки и надо/интересно/полезно искать в реальных(согласно вашему определению) программах

Re: В дополнение

[parse error (from livejournal.com)]

Поможет, отчасти. В случае когда благодаря программе автор узнает, что его программа не завершается, хотя должна. И наоборот.

Re: стоп, стоп...

[109.livejournal.com]

вообще-то, все real world (tm) программы как раз завершаются только при получении сигнала извне. например, десктопные программы завершаются при получении сигнала WM_CLOSE, cloud services (both web roles and worker roles) завершаются при получении сигнала от окружения, windows service завершается при получении сигнала от control manager, и т.д.

получается, на dafny ни одну из этих программ написать нельзя? только учебные примеры в консоли?

Re: стоп, стоп...

[thedeemon.livejournal.com]

За отсутствием IO помимо print и интеграции с остальным .NET'ом, именно написать - нельзя. Можно лишь промоделировать. В прынципе, помимо обычных циклов while и рекурсии, которые обязаны завершаться, там есть еще коиндуктивные типы (см. конец поста), которые могут описывать бесконечные ленивые потоки сообщений, и функции над ними получается могут работать сколь угодно, но должны вести себя определенным образом - обработка каждого конкретного сообщения должна завершаться, и сама корекурсия должна иметь подобающую форму. Это (коиндукция) тоже уже стандартный подход в тотальных языках для описания well-behaved event loops.

В целом же, мне представляется, Dafny нужен для верификации отдельных алгоритмов, а не больших систем целиком.

[anonim-legion.livejournal.com]

Восхитительно. Интересно, есть ли смысл компилировать такое в plain C.

[thedeemon.livejournal.com]

Тут верификатор умеет рассуждать о выделяемых в памяти объектах (например, проверять условия вида "при возвращении из метода все новые указатели из вот этого множества - созданы самим методом, а не скопированы извне"), но про освобождение памяти я тут ничего не видел, полагаются на GC. Т.е. прямая трансляция в Си вряд ли имеет смысл. А отдельные алгоритмы проверить и потом перевести на Си тут несложно самому, я так и хочу делать.

Вот ATS, который во многом похож (там тоже стираемые при компиляции условия и доказательства, есть встроенный солвер для арифметики, хоть и попроще), он сам генерит Си и через него уже делает бинарники. И там есть развитые средства описания работы с памятью на сишном уровне (вроде "эта функция возвращает указатель на непроинициализированный буфер такого-то размера"), там же верификатор следит, чтобы все было аккуратно и однократно освобождено.