🗊Презентация ВЕРИФИКАЦИЯ ПРОГРАММ ДВС

ВЕРИФИКАЦИЯ ПРОГРАММ ДВС Лектор - С.А. Ивановский

Лекция 8 2 http://why3.lri.fr/ Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs. См. Why/Lecture notes.pdf

INRIA (фр. Institut national de recherche en informatique et en automatique, государственный институт исследований в информатике и автоматике) — национальный исследовательский институт во Франции, работающий в области компьютерных наук, теории управления и прикладной математики. Создан в 1967 в Роканкур рядом с Парижем в рамках государственной программы Plan Calcul (англ.). INRIA является научно-технологическим государственным учреждением (établissement public à caractère scientifique et technologique, EPST) и находится под двойным управлением министерства образования и министерства экономики.

Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina)[1] с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ. Coq разработан во Франции в рамках проекта TypiCal (ранее — LogiCal)[2], совместно управляемом INRIA, Политехнической школой, Университетом Париж-юг XI и Национальным центром научных исследований, ранее была выделенная группа и в Высшей нормальной школе Лиона.

The Krakatoa Verification Tool for JAVA programs

Кpaкaта́y — действующий вулкан в Индонезии, расположенный на Малайском архипелаге в Зондском проливе, между островами Ява и Суматра. Площадь островов 10,5 км². Высота нынешнего вулкана 813 м.

The Krakatoa Verification Tool for JAVA programs Инструмент Krakatoa позволяет автоматизировать доказательство корректности программ на языке Java. В качестве языка спецификации он использует подмножество языка JML. Инструмент Krakatoa (в связке с инструментом Why3) генерирует условия верификации, корректности и завершимости для исходного текста программы на Java, снабженного комментариями, в которых описана спецификация, индуктивные утверждения и оценочные функции.

Графическая оболочка инструмента Why3 позволяет управлять доказательством истинности сгенерированных условий: запустить один из инструментов-солверов, разбить условие на части (чтобы доказывать каждую из них по отдельности). Подробнее об этом можно прочитать в описании инструмента Krakatoa (http://krakatoa.lri.fr/krakatoa.html).

2.1 The basics of the methodology public class Lesson1 { /*@ ensures \result >= x && \result >= y && @ \forall integer z; z >= x && z >= y ==> z >= \result; @*/ public static int max(int x, int y) { if (x>y) return x; else return x; } }

2.2 Loop invariants /*@ requires x >= 0; @ ensures @ \result >= 0 && \result * \result <= x @ && x < (\result + 1) * (\result + 1); @*/ public static int sqrt(int x);

/*@ requires x >= 0; @ ensures @ \result >= 0 && \result * \result <= x @ && x < (\result + 1) * (\result + 1); @*/ public static int sqrt(int x) { int count = 0, sum = 1; while (sum <= x) { count++; sum = sum + 2*count+1; } return count; }

public static int sqrt(int x) { int count = 0, sum = 1; /*@ loop_invariant @ count >= 0 && x >= count*count && @ sum == (count+1)*(count+1); @*/ while (sum <= x) { count++; sum = sum + 2*count+1; } return count; }

/*@ loop_invariant @ ... @ loop_variant x  sum; @*/ while (sum <= x) { ...

2.3 Array accesses public class Arrays { /*@ requires t != null && t.length >= 1; @ ensures @ 0 <= \result < t.length && @ \forall integer i; 0<=i<t.length ==> t[i] <= t[\result]; @*/ public static int findMax(int[] t); }

public static int findMax(int[] t) { int m = t[0]; int r = 0; /*@ loop_invariant @ 1 <= i && i <= t.length && 0 <= r && r < t.length && @ m == t[r] && \forall integer j; 0<=j && j<i ==> t[j]<=t[r]; @ loop_variant t.lengthi; @*/ for (int i=1; i < t.length; i++) { if (t[i] > m) { r = i; m = t[i]; } } return r; }

См. далее «! krakatoa.pdf»