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

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

Цитата из википедии: "Миф о Дафне, превратившейся в лавр, зародился в эпоху эллинизма[17]. По некоторому мнению, ему не следует придавать особого значения, поскольку, как считает И. И. Маханьков, он явно позднейшего происхождения и создан с целью объяснить особую роль лавра в культе Аполлона". А, не, не то.

Dafny - это язык программирования, похожий на упрощенный C#/Java/whatever с рядом дополнительных фишек. Там классы (в том числе генерики), объекты, у них поля, методы с императивным кодом, в них переменные, циклы, мутабельные массивы и прочие радости императивного программирования. К этому добавлены индуктивные и коиндуктивные алгебраические типы и паттерн-матчинг по ним. Компилятор из этого генерит C# и из него уже рабочие бинарники, которые можно позапускать. А дальше начинается интересное. В язык включены конструкции для указания пред- и пост-условий методов, ассертов в коде, а также инвариантов циклов и метрик завершимости, причем записываются весьма удобным и человечным языком. И вторая часть компилятора - это верификатор, который все эти условия проверяет статически. Для этого он внутри генерит спецификации на Boogie, который в свою очередь использует SMT-солвер Z3. SMT, как известно, это Sick Magic Trickery, поэтому возможности верификатора к пониманию кода и самостоятельным выводам весьма впечатляют. Это вам не коммутативность сложения доказывать в четырехсотый раз. В результате программы на Dafny как минимум доказанно не вылетают за границы массивов (и вообще никуда не вылетают) и всегда завершаются, а как норма - еще и доказанно делают то, что должны.
( Read more... )