Дафни

Dafny - это императивный скомпилированный язык, предназначенный для C # и поддерживающий предварительные условия формальных спецификаций с по , постусловия, инварианты цикла и варианты цикла. Язык сочетает в себе идеи в основном из функциональной и императивной парадигм и включает ограниченную поддержку объектно-ориентированного программирования. Возможности включают универсальные классы, динамическое размещение, индуктивные типы данных и разновидность логики разделения, известную как неявные динамические кадры для рассуждений о побочных эффектах. Dafny был создан Рустаном Лейно из Microsoft Research после его предыдущей работы по разработке ESC / Modula-3, ESC / Java и Spec #. Dafny широко используется в обучении и регулярно участвует в соревнованиях по проверке программного обеспечения (например, VSTTE'08, VSCOMP'10, COST'11 и VerifyThis'12).

Дафни был разработан, чтобы обеспечить простое введение в формальную спецификацию и проверку, и широко использовался в обучении. Dafny построен на промежуточном языке Boogie , который использует автоматическое средство доказательства теорем Z3 для выполнения обязательств по доказательству.

• 1 Типы данных
• 2 Императивные функции
• 3 Инварианты цикла
• 4 Функции проверки
• 5 Ссылки
• 6 Внешние ссылки

Dafny предоставляет методы для реализации, которые могут иметь побочные эффекты и функции для использования в спецификации чистый. Методы состоят из последовательностей операторов, соответствующих знакомому императивному стилю, тогда как тело функции, напротив, является просто выражением. Любые побочные инструкции в методе (например, присвоение элемента параметра массива) должны быть учтены, отмечая, какие параметры могут быть изменены в предложении модифицирует. Dafny также предоставляет ряд неизменяемых типов коллекций, включая: последовательности (например, seq), наборы (например, set) и карты (map ). Кроме того, предоставляются изменяемые массивы (например, array).

Дафни поддерживает доказательства императивных программ, основанные на идеях логики Хоара. Ниже показано множество таких функций в Dafny, включая использование предварительных условий, постусловий, инвариантов цикла и вариантов цикла.

method max (arr: array ) returns (max: int) // В массиве должен быть хотя бы один элемент, требуется arr! = Null arr.Length>0; // Возвращаемое значение не может быть меньше, чем гарантирует любой элемент в массиве (forall j: int :: (j>= 0 j < arr.Length ==>max>= arr [j])); // Возврат должен соответствовать некоторому элементу в массиве гарантирует (существует j: int :: j>= 0 j < arr.Length max==arr[j]); { max:=arr[0]; var i:int :=1; // while(i < arr.Length) // Indent at most arr.Length (needed to show i==arr.Length after loop) invariant (i<=arr.Length); // No element seen so far larger than max invariant (forall j:int :: j>= 0 j max>= arr [j]); // Некоторый видимый элемент соответствует максимальному инварианту (существует j: int :: j>= 0 j max) {max: = arr [i];} // Продолжаем через массив i: = i + 1; }}

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

Обработка инвариантов цикла в Dafny отличается от традиционной логики Хоара. Переменные, измененные в цикле, обрабатываются таким образом, что (большая часть) информации, известной о них до цикла, отбрасывается. Информация, необходимая для доказательства свойств таких переменных, должна быть явно выражена в инварианте цикла. Напротив, переменные, не измененные в цикле, сохраняют всю информацию, известную о них заранее. Следующее обеспечивает иллюстрацию:

метод sumAndZero (ns: array ) возвращает (sum: nat) требует ns! = Null требуется для всех i :: 0 <= i < ns.Length ==>ns [i]>= 0 изменяет ns {var i : int: = 0; var arr: array : = ns; // потому что параметры не могут быть присвоены sum: = 0; // while (i < arr.Length) { sum := sum + arr[i]; arr[i] := arr[i]; i := i + 1; } }

Проверка не пройдена, потому что Дафни не может установить, что (sum + arr [i])>= 0выполняется при присваивании. Из предварительного условия интуитивно понятно, что forall i: : 0 <= i < arr.Length ==>arr [i]>= 0сохраняется в цикле, поскольку arr [i]: = arr [i];является NOP. Однако это присвоение заставляет Дафни рассматривать arrкак изменяемую переменную и отбрасывать информацию, известную о ней до цикла. Чтобы проверить эту программу в Dafny, мы можем: удалить избыточное присвоение arr [i ]: = arr [i];; или добавьте инвариант цикла , инвариант forall i :: 0 <= i < arr.Length ==>arr [i]>= 0

список типов данных = Nil | Link (data: int, next: List) function sum (l: List): int {match l case Nil =>0 case Link (d, n) =>d + sum (n)} predicate isNatList (l: List) {match l case Nil =>true case Link (d, n) =>d>= 0 isNatList (n)} Призрачный метод NatSumLemma (l: List, n: int) требует isNatList (l) n == sum ( l) гарантирует, что n>= 0 {соответствует l case Nil =>// Разряжается автоматически case Link (data, next) =>{// Применить индуктивную гипотезу NatSumLemma (next, sum (next)); // Проверяем, что известно Dafny assert data>= 0; }}