Дафни

Дафни

Парадигма	Императивный , функциональный
Разработано	К. Рустан М. Лейно
Разработчик	Исследования Майкрософт , AWS
Впервые появился	2009 год ( 2009 )
Стабильная версия	3.7.2 / 14 июля 2022 г ( 14.07.2022 )
Дисциплина набора текста	Статичный, прочный, безопасный
Лицензия	МОЯ лицензия
Расширения имен файлов	.dfy
Веб-сайт	дурак .org

Dafny — это императивный и функциональный компилируемый язык , который компилируется в другие языки программирования , такие как C# , Java , JavaScript , Go и Python . Он поддерживает формальную спецификацию посредством предусловий , постусловий , инвариантов цикла , вариантов цикла , спецификаций завершения и спецификаций кадрирования чтения/записи. Язык сочетает в себе идеи функциональной и императивной парадигм; он включает поддержку объектно-ориентированного программирования . Возможности включают в себя общие классы , динамическое размещение , индуктивные типы данных и вариацию логики разделения, известную как неявные динамические кадры. для рассуждений о побочных эффектах. Dafny был создан Рустаном Лейно из Microsoft Research после его предыдущей работы над разработкой ESC/Modula-3, ESC/Java и Spec#.

Дафни широко используется в обучении. потому что он обеспечивает простое и интегрированное введение в формальную спецификацию и проверку; он регулярно участвует в конкурсах по верификации программного обеспечения (например, VSTTE'08, ВСКОМП'10, СТОИМОСТЬ'11, и VerifyThis'12 ).

Dafny был разработан как язык программирования, поддерживающий проверку, требующий проверки наряду с разработкой кода. Таким образом, он соответствует парадигме разработки программного обеспечения «Исправление по конструкции». Доказательства проверки поддерживаются набором математических инструментов, который включает в себя математические целые и действительные числа, битовые векторы, последовательности, множества, мультимножества, бесконечные последовательности и множества, индукционные, коиндукционные и вычислительные доказательства. Обязательства по проверке выполняются автоматически при наличии достаточной спецификации. Дафни использует некоторый анализ программы, чтобы сделать вывод о многих утверждениях спецификации, уменьшая нагрузку на пользователя по написанию спецификаций. Общая схема доказательства – это логика Хоара .

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

Типы данных

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

Обязательные особенности

Следующее иллюстрирует многие функции Dafny, включая использование предусловий, постусловий, инвариантов и вариантов цикла.

method max(arr:array<int>) returns (max:int)
 // Array must have at least one element
 requires arr.Length > 0
 // Return cannot be smaller than any element in array
 ensures forall j : int ::   j >= 0 && j < arr.Length  ==>  max >= arr[j]
 // Return must match some element in array
 ensures exists j : int ::   j>=0 && j < arr.Length && max == arr[j]
{
  max := arr[0];
  var i: int := 1;
  //
  while(i < arr.Length)
  // Index 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 < i  ==>  max >= arr[j]
  // Some element seen so far matches max
  invariant exists j:int :: j >= 0 && j < i && max == arr[j]
  // arr.Length - i decreases at every step and is lower-bounded by 0
  decreases arr.Length - i
  {
    // Update max if larger element encountered
    if (arr[i] > max) {
      max := arr[i];
    }
    // Continue through array
    i := i + 1;
  }
}

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

Инварианты цикла

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

method sumAndZero(arr: array<int>) returns (sum: nat)
  requires forall i :: 0 <= i < arr.Length  ==>  arr[i] >= 0
  modifies arr
{
  var i: int := 0;
  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]; это НОП . Однако это задание заставляет Дафни лечить arr как изменяемую переменную и удалить информацию, известную о ней до цикла. Чтобы проверить эту программу в Dafny, мы можем либо (а) удалить избыточное присваивание arr[i] := arr[i];; или (б) добавить инвариант цикла invariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0

Дафни дополнительно использует ограниченный статический анализ для вывода простых инвариантов цикла, где это возможно. В приведенном выше примере может показаться, что инвариант цикла invariant i >= 0 также требуется как переменная i мутирует внутри цикла. Хотя базовая логика действительно требует такого инварианта, Дафни автоматически выводит его, и, следовательно, его можно опустить на исходном уровне.

Особенности доказательства

Dafny включает функции, которые дополнительно поддерживают его использование в качестве помощника по проверке . Хотя доказательства простых свойств в пределах function или method (как показано выше) не являются чем-то необычным для инструментов такого рода, Дафни также позволяет доказывать свойства между одним function и еще один. Как это обычно бывает с помощником по доказательству , такие доказательства часто носят индуктивный характер. Дафни, возможно, необычно использует вызов метода в качестве механизма применения индуктивной гипотезы. Ниже показано:

datatype List = 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)
}

lemma NatSumLemma(l: List, n: int)
  requires isNatList(l) && n == sum(l)
  ensures n >= 0 
{
  match l
    case Nil =>
      // Discharged Automatically
    case Link(data, next) => {
      // Apply Inductive Hypothesis
      NatSumLemma(next, sum(next));
      // Check what known by Dafny
      assert data >= 0;
    }
}

Здесь, NatSumLemma доказывает полезное свойство между sum() и isNatList() (т.е. что isNatList(l) ==> (sum(l) >= 0)). Использование ghost method для кодирования лемм и теорем является стандартным в Дафни с использованием рекурсии для индукции (обычно структурной индукции ). Анализ случая проводится с использованием match утверждения и неиндуктивные случаи часто сбрасываются автоматически. Верификатор также должен иметь полный доступ к содержимому файла. function или predicate чтобы развернуть их по мере необходимости. Это имеет значение при использовании вместе с модификаторами доступа . В частности, скрытие содержимого function используя protected Модификатор может ограничить, какие свойства могут быть установлены для него.

См. также

• Проектирование по договору

Дальнейшее чтение

• Мейер, Бертран; Нордио, Мартин, ред. (2012). Инструменты для практической верификации программного обеспечения: Международная летняя школа, LASER 2011, остров Эльба, Италия, Пересмотренные учебные лекции . Спрингер . ISBN  978-3642357459 .
• Ситниковский, Боро (2022). Знакомство с проверкой программного обеспечения с помощью Dafny Language: проверка корректности программы . Апресс. ISBN  978-1484279779 .

Внешние ссылки

• Dafny: средство проверки работоспособности языка и программ — Microsoft Research
• GitHub — dafny-lang/dafny: Dafny — это язык программирования, поддерживающий проверку.