Лекция Виды формальных спецификаций. Практические задачи курса

2 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Виды использования моделей жизненном цикле ПО

3 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Пример: Разработка спецификации для целей прототипирования В примере не будет рассматриваться задача «оценки реализуемости».

4 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 «Очередь» - Неформальное описание системы Требуется спроектировать систему, реализующую операции для работы с «очередями» Система будет предоставлять программный интерфейс (ПИ, или Application Program Interface - API)

5 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Первый шаг формализации. Выбор терминов (денотатов) Типы данных Очередь - Queue Элемент очереди - Element Операции Поставить в очередь - append Кого обслуживать следующим? - first Кто останется после этого? - rest Константа Пустая очередь - empty

6 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Сигнатура (структура) интерфейса - простейший вид спецификации QUEUE = class type Element, Queue value empty : Queue, append : Element > Queue, first : Queue -~-> Element, rest : Queue -~-> Queue end Мы описали структуру, то есть набор элементов и связи между элементами.

7 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Упражнение: Как бы я написал(а) спецификацию очереди Знаю Оцениваю сам Оцениваю по отношению к сформулированным требованиям

8 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Требования к спецификации. Спецификация должна: быть простой/естественной для реализитора/пользователя/ дизайнера тестов/тестировщика/ менеджера требований и инженера по качеству позволять проверять внутреннюю согласованность/консистентность быть недвусмысленной для объективности анализа быть полной (определена область допустимых значений для всех функций, поведение определено при всех допустимых сценариях использования) не содержать лишних ограничений на реализацию Вопрос: какие из этих требований могут быть ослаблены?

9 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Известные виды спецификаций Алгебраические/аксиоматические Явные/исполнимые/алгоритмические Неявные/неисполнимые/ограничения

10 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Очередь. Алгебраическая спецификация QUEUE = class type Element, Queue value empty: Queue, append : Element > Queue, first : Queue -~-> Element, rest : Queue -~-> Queue axiom 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 e else first(q) end, rest(append(e,q)) is if q=empty then empty else append(rest(q)) end end

11 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Пример трансформаций типа re-writing … axiom 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 e else first(q) end, rest(append(e,q)) is if q=empty then empty else append(e, rest(q)) end end rest(append(a, append (b, empty))) append(a, rest(append (b, empty))) append(a, empty)

12 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Очередь. Явная спецификация QUEUE = class type Element, Queue = Element-list value empty: Queue, append : Element > Queue, first : Queue -~-> Element, rest : Queue -~-> Queue axiom forall e : Element, q : Queue :- empty is, append(e,q) is q ^, first(q) is hd q pre q~=, rest(q) is tl q pre q~= end

13 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Очередь. Явная спецификация (зеркало)... axiom forall e : Element, q : Queue :- empty is, append(e,q) is ^ q, first(q) is q(len q) pre q~=, rest(q) is variable x: Queue = for i = do x:=x ^ q(i) end pre q~= end

14 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Очередь. Неявная спецификация QUEUE = class type Element, Queue = Element-list value empty: Queue, append : Element > Queue, first : Queue -~-> Element, rest : Queue -~-> Queue axiom forall e : Element, q : Queue :- empty is, append(e,q1) as post q1 ^ = q2, first(q) as e post hd q= e pre q~=, rest(q1) as q2 post exists e : Element :- ^ q2 = q1 pre q~=, end

15 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Очередь. Неявная спецификация (зеркало) QUEUE = class type Element, Queue = Element-list value empty: Queue, append : Element > Queue, first : Queue -~-> Element, rest : Queue -~-> Queue axiom forall e : Element, q : Queue :- empty is, append(e,q1) as q2 post ^ q1 = q2, first(q1) as e post exists q2 : Queue :- q2 ^ = q1 pre q1~=, rest(q1) as q2 post tl q1= q2 pre q1~= end

16 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Определение функции 1. Определить имя функции 2. Определить тип (сигнатуру) тип аргументов тип результата всюду вычислимая (total) или частично вычислимая (partial) 3. Определить стиль описания явное определение (explicit) – если можем предложить формулу неявное определени (implicit) – если можем описать input-output отношение аксиоматическое (алгебраическое) – всегда возможно типичное использование в случае, когда приходится использовать специфический вид аргументов (аргумент – вызов функции), например, f(g(x),x) - h(f,x)

17 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Практические цели курса. Научиться: Строить модели сопоставлять модели с неформальными требованиями Изменять уровень абстракции (повышать и понижать уровень) Анализировать модели (проверять их консистентность) Анализировать согласованность моделей, при помощи: Уточнения (refinement) Тестирования

18 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Аналоги курса SE313 Формальные методы программной инженерии Подходы к проектированию и построению программного обеспечения, использующие математический аппарат для достижения высоких уровней качества. Математические основы формальных методов; формальное моделирование; аттестация формальных моделей; формальный анализ проектирования; преобразование программ.

19 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Аналоги курса SE221 Тестирование программного обеспечения Подробный курс по всем аспектам тестирования, а также по другим аспектам верификации и аттестации, включая определение тестируемых требований, рецензий и обеспечение качества продукта.

20 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Рекомендации Важнейшей задачей проектов по разработке программного обеспечения {software projects} является разрешение проблем заказчика как явных, так и неявных. К сожалению, наиболее частой ошибкой является фокусирование исключительно на технических проблемах, что в дальнейшем приводит к созданию непригодных для использования систем.

21 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Рекомендации Реккурентно. Измерение {measurement}, количественный анализ {quantification} и формальные {formal} математические подходы. Моделирование, представление {representation} и абстракция {abstraction}. Человеческие факторы и удобство использования{usability}. Необходимо снова и снова обращать внимание студентов на то, что программная инженерия {Software engineering} - это больше, чем просто технология {not just about technology}. Важность масштабирования {importance of scale}: студенты могут практиковаться на решении относительно небольших проблем, однако они должны понимать, что возможности множества методов наиболее полно проявляются в больших системах. Они должны быть готовы решать задачи, как если бы они работали над очень большими системами, они также должны учиться читать и понимать код больших систем. Рекомендация 5. Изучение некоторых тем программной инженерии {software engineering} подразумевает определенный уровень зрелости {maturity}.

22 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Языки и методологии спецификаций Языки Методологии RSLRAISE VDM-SLVDM VDM++Development process for real- time systems (IFAD) Z, B, ASML EiffelDesign-by-contract ADL/ADL2, JML, Jatva, Spec# Design-by-contract iContractDesign-by-contract Abstract State Machines B-Method Estelle Esterel Lotos Overture Modeling Language Petri Nets Promela RAISE SDL VDM Z

23 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Спецкурс В.В.Кулямина. Технология программирования. Компонентный подход.

24 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Ключевые слова

25 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Дополнительная литература Б.Мейер. Программная инженерия как предмет обучения.- Открытые системы, Июль-Август 2001, стр Бертран Мейер. Объектно- ориентированное конструирование программных систем (+ CD-ROM)// Русская редакция, 2005.

26 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Приложение

27 ВМиК МГУ. Сентябрь-декабрь 2006 А.К.Петренко. Формальные спецификации программ - I. Лекция 2 Пример алгебраических спецификаций. База данных DATABASE = class type Database, Key, Data value /* generators */ empty: Database, insert : Key > Database, remove : Key > Database, /* observers */ defined : Key > Bool, lookup : Key > Data axiom [defined-empty] k : Key defined(k,empty) = false, [ defined-insert ] k,k1 : Key, d : Data, db : Database defined(k,insert(k1,d,db)) is (k = k1) \/ defined(k,db), [defined-remove] k,k1 : Key, db : Database defined(k,remove(k1)db)) is k ~= k1 /\ defined(k,db), [lookup-insert] k,k1 : Key, d : Data, db : Database lookup(k,insert(k1,d,db)) = if k = k1 then d else lookup(k,db) end pre k = k1 V defined(k,db), [lookup-remove] k,k1 : Key, db : Database lookup(k,remove(k1,db)) lookup(k,db) pre k~=k1/\ defined(k,db) end