lecture-2

Формальная спецификация иверификация программ.Лекция 2.Виды формальных спецификацийА.К.Петренко, А.В.Хорошилов,Е.В.КорныхинМГУ ВМК, ИСП РАНhttp://sp.cmc.msu.ru/courses/fmspОсень, 2012Элементы Основанийразработки программРазделение понятийРеализации программы (алгоритма) иПоведения программыАбстракцияВиды абстракцииМетоды изменения уровня абстракции исопоставления уровней2Формальные методыСпецификация (поведения)Языки формальной спецификацииИнструменты поддержкиАнализ корректности спецификацииАнализ соответствия спецификации иреализации (верификация)Анализ соответствия разных уровнейабстракции, разных моделейОтслеживание связей с требованиями,функциями реализации, тестами и др.3Для чего нужны спецификацииПомощь в дизайне (уточнить треб, вскрыть открытыевопросы и противоречия в треб/проекте архитектурыЗафиксировать проектные решения для передачи знаний(целевой продукт реверс-инженерии)Альтернативная информационная структура для анализасистемы (корректность, сравнение полноты с реализацией,критерии качества/полноты верификации)«Мечта/идеал» – генерация программ по спецификации(не всегда целевых программ, например, тестов, доказательств(evidence))ВМК МГУ.Сентябрь-декабрь 20124Где нужны спецификацииТам, где нет готовых шаблонных решенийБольшой круг разработчиков/пользователей =>задача фиксации и передачи знаний о системеОтветственное SW/HW, задачи надежности иотслеживания требованийВМК МГУ.Сентябрь-декабрь 20125Зачем нужны языкиспецификаций?Можно ли рассматривать программуна Java или Си как спецификацию ?В чем плюсы введения специальныхязыков спецификации?В чем минусы введения языковспецификации?ВМК МГУ.Сентябрь-декабрь 20126Пример: «Очередь» Неформальное описание системыТребуется спроектировать систему,реализующую операции для работы с«очередями»Система будет предоставлятьпрограммный интерфейс (ПИ, илиApplication Program Interface - API)ВМК МГУ.Сентябрь-декабрь 20127Первый шаг формализации.Выбор терминов (денотатов)Типы данныхОперацииОчередь - QueueЭлемент очереди - ElementПоставить в очередь - appendКого обслуживать следующим? - firstКто останется после этого? - restКонстантаПустая очередь - emptyВМК МГУ.Сентябрь-декабрь 20128Известные виды спецификацийАлгебраические/аксиоматическиеЯвные/исполнимые/алгоритмическиеНеявные/неисполнимые/ограниченияВМК МГУ.Сентябрь-декабрь 20129Сигнатура (структура) интерфейса- простейший вид спецификацииscheme QUEUE = classtypeElement,Queuevalueempty : Queue,append : Element >< Queue -> Queue,first : Queue -~-> Element,rest : Queue -~-> QueueendМы описали структуру, то есть наборэлементов и связи между элементами.ВМК МГУ.Сентябрь-декабрь 201210Очередь.

Алгебраическаяспецификация на RSLscheme QUEUE = classtypeElement,Queuevalueempty: Queue,append : Element >< Queue -> Queue,first : Queue -~-> Element,rest : Queue -~-> Queueaxiom forall e : Element, q : Queue :empty ~= append (e,q),first(append(e, empty)) is e,rest(append(e,empty)) is empty,first(append(e, q)) is if q=empty then eelse first(q) end,rest(append(e,q)) is if q=empty then emptyelse append(e, rest(q)) endendВМК МГУ.Сентябрь-декабрь 201211Интерпретация аксиомыfirst(append(e, empty)) is e«очередь»emptyсценарийget value of «e»eappend (e)first ( )result2result2 = eВМК МГУ.Сентябрь-декабрь 2010А.К.Петренко. Формальные спецификациипрограмм - I. Лекция 212Очередь.Явная спецификация на RSLscheme QUEUE = classtypeElement,Queue = Element-listvalueempty: Queue,append : Element >< Queue -> Queue,first : Queue -~-> Element,rest : Queue -~-> Queueaxiom forall e : Element, q : Queue :empty is <..>,append(e,q) is q ^ <.e.>,first(q) is hd q pre q~=<..>,rest(q) is tl q pre q~=<..>endВМК МГУ.Сентябрь-декабрь 201213Очередь.Неявная спецификация на RSLscheme QUEUE = classtypeElement,Queue = Element-listvalueempty: Queue,append : Element >< Queue -> Queue,first : Queue -~-> Element,rest : Queue -~-> Queueaxiom forall e : Element, q : Queue :empty is <..>,append(e,q) as q1 post q ^ <.e.> = q1,first(q) as epost hd q= e pre q~=<..>,rest(q) as q1post exists e : Element :- <.e.> ^ q1 = qpre q~=<..>endВМК МГУ.Сентябрь-декабрь 201214Очередь.

Явная спецификацияс состоянием на RSLscheme QUEUE = classtypeElement,Queue = Element-listvariablequeue : Queue := emptyvalueempty: Queue,append : Element -> write queue Queue,first : Unit -~-> read queue Element,rest : Unit -~-> read queue Queueaxiom forall e : Element :empty is <..>,append(e) is (queue := queue ^ <.e.>;queue),first() is hd queue pre queue~=<..>,rest() is tl queue pre queue~=<..>endВМК МГУ.Сентябрь-декабрь 201215Очередь. Неявнаяспецификация с состояниемscheme QUEUE = classtypeElement,Queue = Element-listvariablequeue : Queue := emptyvalueempty: Queue,append : Element -> write queue Queue,first : Unit -~-> read queue Element,rest : Unit -~-> read queue Queueaxiom forall e : Element :empty is <..>,append(e) as q2 post queue = q2 /\ queue` ^ <.e.> = q2,first() as epost hd queue = e pre queue ~=<..>,rest() as q2post exists e : Element :- <.e.> ^ q2 = queuepre queue~=<..>,endВМК МГУ.Сентябрь-декабрь 201216Очередь.Интерфейс класса на Dafnyclass Queue<T>{// create queue without elementsconstructor empty()// append `e' to the end of queuemethod append(e : T)// get first elementmethod first() returns (e : T)// remove first elementmethod rest()}ВМК МГУ.Сентябрь-декабрь 2012Попробовать в браузере:http://rise4fun.com/Dafny/GYsl0(нажать “ask dafny”)17Очередь.Явная спецификация на Dafnyclass Queue<T>{var elements : seq<T>;method first() returns (e : T)requires |elements| > 0;{return elements[0];}constructor empty()modifies this;{elements := [];}method append(e : T)modifies this;{elements := elements + [e];}ВМК МГУ.Сентябрь-декабрь 2012method rest()requires |elements| > 0;modifies this;{elements := elements[1..];}}Попробовать в браузере:http://rise4fun.com/Dafny/hzIe18Очередь.

Неявнаяспецификация на Dafnyclass Queue<T>{var elements : seq<T>;method first() returns (e : T)requires |elements| > 0;ensures e == elements[0];ensures elements ==old(elements); // needed?constructor empty()modifies this;ensures |elements| == 0;method append(e : T)modifies this;ensures old(elements) + [e] ==elements;ВМК МГУ.Сентябрь-декабрь 2012method rest()modifies this;requires |elements| > 0;ensures old(elements)[1..] ==elements;}Попробовать в браузере:http://rise4fun.com/Dafny/tuQY19Очередь.

Алгебраическаяспецификация на Dafny –параметризованные тестыclass Queue<T>{constructor empty()static method test_1(q :Queue<T>, e : T)modifies q;requires q != null;requires q.non_empty();method append(e : T)modifies this;{var f1 := q.first();method first() returns (e : T)q.append(e);requires non_empty();var f2 := q.first();assert f1 == f2;method rest()}requires non_empty();modifies this;static method test_2(q :Queue<T>, e : T)modifies q;requires q != null;requires !q.non_empty();{q.append(e);var f := q.first();assert f == e;}}function non_empty() : boolreads this;ВМК МГУ.Сентябрь-декабрь 2012Попробовать в браузере:http://rise4fun.com/Dafny/gHI420Очередь.

Эффективная реализацияна Dafny (без постусловий)class Node<T>{var value : T;var next : Node<T>;}// unbounded queueclass Queue<T>{var head : Node<T>;var last : Node<T>;constructor empty()modifies this;{head := null;last := null;}ВМК МГУ.Сентябрь-декабрь 2012method append(e : T)method rest()modifies this, (if last ==requires head != null;null then {} else {last});modifies this;{{if (last == null) {if (head == last) {last := new Node<T>;head := null;head := last;last := null;} else {} else {last.next := new Node<T>;head := head.next;last := last.next;}}}last.value := e;last.next := null;}} // end of Queuemethod first() returns (e : T)requires head != null;{return head.value;}В браузере:http://rise4fun.com/Dafny/gHI421Очередь. Эффективная реализацияна Dafny (c постусловиями)Текст программы со спецификационнымианнотациями настолько большой, что непоместился на слайд.

Смотреть в браузере тут:http://rise4fun.com/Dafny/sllmpВМК МГУ.Сентябрь-декабрь 201222.