ВЕРИФИКАЦИЯ ПРОГРАММ ДВС

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

05.05.2015

Платформа Why / Krakatoa

государственный институт исследований в информатике и автоматике) — национальный исследовательский институт

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

05.05.2015

Платформа Why / Krakatoa

язык функционального программирования (Gallina)[1] с зависимыми типами. Позволяет записывать математические

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

05.05.2015

Платформа Why / Krakatoa

в Зондском проливе, между островами Ява и Суматра. Площадь островов

10,5 км². Высота нынешнего вулкана 813 м.

05.05.2015

Платформа Why / Krakatoa

корректности программ на языке Java.
В качестве языка спецификации он

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

05.05.2015

Платформа Why / Krakatoa

запустить один из инструментов-солверов, разбить условие на части (чтобы доказывать

каждую из них по отдельности). Подробнее об этом можно прочитать в описании инструмента Krakatoa (http://krakatoa.lri.fr/krakatoa.html).

05.05.2015

Платформа Why / Krakatoa

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;
}
}

0 && \result * \result

(\result + 1) * (\result + 1);
@*/
public static int sqrt(int x);

\result * \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;
}

= 1;
/*@ loop_invariant
@ count >= 0 && x >= count*count

&&
@ sum == (count+1)*(count+1);
@*/
while (sum <= x) {
count++;
sum = sum + 2*count+1;
}
return count;
}

{
...

&& t.length >= 1;
@ ensures
@ 0

&&
@ \forall integer i; 0<=i t[i] <= t[\result];
@*/
public static int findMax(int[] t);
}

= 0;
/*@ loop_invariant
@ 1

&& 0 <= r && r < t.length &&
@ m == t[r] && \forall integer j; 0<=j && j 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;
}