Дафни

Дафни

Парадигма	Императивный , функциональный
Разработано	К. Рустан М. Лейно
Разработчик	Исследования Майкрософт , 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, включая использование предусловий, постусловий, инвариантов и вариантов цикла.

метод   max  (  arr  :  array  <int>  )  Массив  )   return   (  max  :  int  arr   должен содержать хотя бы один элемент   требует   //  .  Длина   >   0   // Возвращаемый результат не может быть меньше любого элемента в массиве   , что гарантирует   forall   j   :   int   ::     j   >=   0   &&   j   <   arr  .  Длина    ==>    max   >=   arr  [  j  ]   // Возвращаемый результат должен соответствовать некоторому элементу в массиве   , что гарантирует   существование   j   :   int   ::     j  >=  0   &&   j   <   arr  .  Длина   &&   max   ==   arr  [  j  ]  {    max   :  =   arr  [  0  ]  ;    вар   я  :   int   :  =   1  ;    //    while  (  i   <   arr  .  Длина  )    // Индекс не более arr.Length (необходим для отображения i==arr.Length после цикла)    инвариант   i   <=   arr  .  Длина    // Пока ни один элемент не превышал максимальный    инвариант   forall   j  :  int   ::   j   >=   0   &&   j   <   i    ==>    max   >=   arr  [  j  ]    // Какой-то элемент, замеченный до сих пор, соответствует максимальному    инварианту   существующему   j  :  int   ::   j   >=   0   &&   j   <   i   &&   max   ==   arr  [  j  ]    // arr.Length - i уменьшается на каждом шаге и ограничено снизу 0,    уменьшает   arr  .  Длина   -   i    {      // Обновляем максимум, если встречается элемент большего размера      if   (  arr  [  i  ]   >   max  )   {        max   :  =   arr  [  i  ]  ;      }      // Продолжение обработки массива      i   :  =   i   +   1  ;    }  } 

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

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

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

метод   sumAndZero  (  arr  :   array  <int> ​  <  )   возвращает   (  sum  :   nat  )    требует   forall   i   ::   0   =   i   <   arr  .  Длина    ==>    arr  [  i  ]   >=   0    изменяет   arr  {    var   i  :   int   :  =   0  ;    сумма   :  =   0  ;    //    while  (  i   <   arr.Length ​ ​  )   {      sum   :  =   sum   +   arr  [  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 и еще один. Как это обычно бывает с помощником по доказательству , такие доказательства часто носят индуктивный характер. Дафни, возможно, необычно использует вызов метода в качестве механизма применения индуктивной гипотезы. Ниже показано:

 типов данных  список   =   Nil   |   Link  (  data  :   int  ,   next  :   List  )  функция   sum  (  l  :   List  ):   int   {    match   l      case   Nil   =>   0      case   Link  (  d  ,   n  )   =>   d   +   sum  (  n  )  }  предикат   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   {    match   l      case   Nil   =>        // Автоматически разряжается      case   Link  (  data  ,   next  )   =>   {        // Применяем индуктивную гипотезу        NatSumLemma  (  next  ,   sum  (  next  ));        // Проверяем, что известно Дафни,        утверждают   данные   >=   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 — это язык программирования, поддерживающий проверку.