ВЕРИФИКАЦИЯ ПРОГРАММ ДВС - презентация, доклад, проект скачать

Нажмите для полного просмотра!

Содержание ▲

Вы можете ознакомиться и скачать презентацию на тему ВЕРИФИКАЦИЯ ПРОГРАММ ДВС. Доклад-сообщение содержит 17 слайдов. Презентации для любого класса можно скачать бесплатно. Если материал и наш сайт презентаций Mypresentation Вам понравились – поделитесь им с друзьями с помощью социальных кнопок и добавьте в закладки в своем браузере.

Слайды и текст этой презентации

Слайд 1

Описание слайда:

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

Слайд 2

Описание слайда:

Лекция 8 2 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

Слайд 3

Описание слайда:

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

Слайд 4

Описание слайда:

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

Слайд 5

Описание слайда:

Слайд 6

Описание слайда:

The Krakatoa Verification Tool for JAVA programs

Слайд 7

Описание слайда:

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

Слайд 8

Описание слайда:

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

Слайд 9

Описание слайда:

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

Слайд 10

$2.1 The basics of the methodology public class Lesson1 { /*@ ensures \result >= x && \result >= y && @ \forall integer z; z >= x && z >= y ==> z >=...$

Описание слайда:

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

Слайд 11

$2.2 Loop invariants /*@ requires x >= 0; @ ensures @ \result >= 0 && \result * \result$

Описание слайда:

2.2 Loop invariants /*@ requires x >= 0; @ ensures @ \result >= 0 && \result * \result

Слайд 12

$/*@ requires x >= 0; @ ensures @ \result >= 0 && \result * \result$

Описание слайда:

/*@ requires x >= 0; @ ensures @ \result >= 0 && \result * \result

Слайд 13

$public static int sqrt(int x) { int count = 0, sum = 1; /*@ loop_invariant @ count >= 0 && x >= count*count && @ sum == (count+1)*(count+1); @*/...$

Описание слайда:

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