lecture-2 (811285)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Формальная спецификация иверификация программ.Лекция 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.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций