Учебное пособие по методам Флойда

Д.В. Буздалов, Е.В. Корныхин, А.А. Панфёров,А.К. Петренко, А.В. ХорошиловПРАКТИКУМ ПОДЕДУКТИВНОЙВЕРИФИКАЦИИПРОГРАМММосква2014УДК 004.415.5ББК 32.973-18Печатается по решению Редакционно-издательского Совета факультетавычислительной математики и кибернетикиМГУ имени М.В. ЛомоносоваРецензенты:И.В. Машечкин, профессор, д.ф.-м.н.С.Ю. Соловьев, профессор, д.ф.-м.н.Д.В. Буздалов, Е.В. Корныхин, А.А, Панфёров, А.К.

Петренко, А.В.Хорошилов.Практикум по дедуктивной верификации программ: учебно-методическоепособие. — М. Издательский отдел факультета ВМК МГУ имени М.В. Ломоносова (лицензия ИД № 05899 от 24.09.2001); МАКС Пресс, 2014. — 97 с.ISBN 978-5-89407-531-0ISBNДанное пособие посвящено основным понятиям дедуктивной верификации последовательных программ. Дедуктивная верификация позволяет формальнообосновать, что программа выполняет формализованные требования путем построения набора утверждений и доказательства их истинности. В качестве методов дедуктивной верификации в пособии рассматриваются методы Флойда(или Хоара-Флойда). Пособие рекомендуется студентам, осваивающим методыформальной верификации программ, а также аспирантам и преподавателям.УДК 004.415.5ББК 32.973-18This textbook is devoted to foundations of deductive verification of software.Deductive verification is aimed to prove that a program under verification consistswith function requirements by proving some theorems about behavior of thisprogram.

R. Floyd's methods are using as an example of deductive verificationmethods. The textbook is aimed at students learning the formal verification ofsoftware and at postgraduate students and lecturers.Ключевые слова: формальная спецификация, формальная верификация, дедуктивная верификация, методы Флойда, формальные методы разработки программ.Keywords: formal specification, formal verification, deductive verification, Floyd'smethods, formal methods of software development.ISBN 978-5-89407-531-0ISBN© Факультет вычислительной математики икибернетики МГУ имени М.В.Ломоносова,2014© Буздалов Д.В., Корныхин Е.В., ПанфёровА.А., Петренко А.К., Хорошилов А.В., 20142Оглавление1 Методы верификации Флойда......................................................................51.1 Математическая модель программы...................................................6Переменные программы............................................................................6Операторы программы...............................................................................7Блок-схемы.....................................................................................................9Семантика блок-схем...............................................................................12Задачи и упражнения...............................................................................141.2 Математическая модель требований.................................................16Входной и выходной предикаты..........................................................17Задачи и упражнения...............................................................................171.3 Задача верификации................................................................................19Частичная и полная корректность программ.................................19Верификация программы целочисленного деления....................20Задачи и упражнения...............................................................................251.4ФормулировкаметодовФлойдадлядоказательствакорректности программ.................................................................................27Метод индуктивных утверждений Флойда.....................................28Метод фундированных множеств Флойда......................................34Замечания к методам Флойда..............................................................37Доказательствополнойкорректностипрограммыцело-численного деления при помощи методов Флойда.......................38Задачи и упражнения...............................................................................422 Практикум по методам Флойда.................................................................562.1 Ещё один пример доказательства полной корректности ........5632.2 Один подход к построению индуктивных утверждений иоценочных функций.......................................................................................612.3 Задачи на метод индуктивных утверждений................................672.4 Задачи на метод фундированных множеств..................................702.5 Общие задачи.............................................................................................75Литература ...........................................................................................................9741 Методы верификации ФлойдаДанное пособие является введением в методы дедуктивной верификации последовательных программ (или, как ее еще называют,аналитической верификации).Целью любой верификации программы (и, в частности, дедуктивной верификации) является установление соответствия программы ее требованиям.

Дедуктивная верификация устанавливаетэто соответствие в виде логического вывода утверждения о том,что программа соответствует требованиям. При этом доказываетсясоответствие программы требованиям на всех входах программы. Вотличие от этого, например, в таком методе верификации как тестирование программа проверяется лишь при некоторых входахпрограммы (тестах).Далее, без ограничения общности, под «методами верификации»будут пониматься «дедуктивные методы верификации».Поскольку дедуктивная верификация основана на использовании логических (математических) заключений, она должна оперировать с математическими («формальными») моделями как программ, требований, так и с формально определенным отношениемих соответствия.Мы начнем рассмотрение методов верификации на простейшихмоделях последовательных программ. Первая модель будет соответствовать программам, написанным на структурном языке программирования• без массивов;• без использования адресной арифметики;• без рекурсии (вызова подпрограмм);5• без взаимодействия с окружением (например, посредствомоператоров ввода-вывода).Методы верификации рекурсивных программ не входят в материал лекций.Программы, взаимодействующие с окружением, относятся к параллельным (или, как их еще называют, реактивным) программами мы их тоже пока не рассматриваем.Мы рассмотрим методы верификации последовательных программ, которые называют методами Флойда (или методами Флойда-Хоара).

Корни этих методов уходят к Алану Тьюрингу, которыйв своей лекции Лондонскому математическому обществу в 1947впервые озвучил идею индуктивных утверждений. До полноценныхметодов верификации эта идея была доведена независимо Робертом Флойдом [1] и Тони Хоаром [2] в конце 60-х годов 20 века.

Вданном пособии изложение этих методов следует их трактовке вмонографиях [5] и [6].1.1 Математическая модель программыОписание математической модели мы начнем с несколькихвспомогательных определений.Переменные программыКаждая программа работает с конечным числом переменных.Переменные разделяются на три типа: входные, промежуточные ивыходные. Вектора этих переменных мы будем обозначать x = ( x1,x2, …, xa ), y = ( y1, y2, …, yb ) и z = ( z1, z2, …, zc ) соответственно.Входные переменные содержат исходные входные значение и никогда не меняются во время работы программы. Промежуточные6переменные используются для хранения промежуточных результатов в процессе вычисления.

Выходные переменные содержат значения, вычисляемые данной программой. Далее, если не будет сказано специально, входные переменные будем обозначать как x1, x2, …,промежуточные как y1, y2, …, выходные как z1, z2, … .Каждая переменная v может принимать значения из некоторогомножества Dv, которое называется доменом переменной. Также, мыбудем выделять три непустых домена:• входной домен Dx = Dx1  Dx2  …  Dxa• домен программы Dy = Dy1  Dy2  …  Dyb• выходной домен Dz = Dz1  Dz2  …  DzcМножество значений всех возможных переменных образуетуниверсальный домен D.

Это значит, что для любой переменной vвыполнено соотношение: Dv  D. Кроме того, мы выделим два специальных значения: Т (истина) и F (ложь). Функции, принимающие значения только из множества {Т, F}, мы будем называть предикатами на области определения функции.

Напомним, что функцией из некоторого множества Х в некоторое множество Y называется отображение, ставящее каждому элементу множества X некоторый элемент множества Y единственным образом.Расширенным доменом Dv+ переменной v будем называть доменэтой переменной, дополненный специальным значением , котороене входит в универсальный домен: Dv+ = Dv  {}.Операторы программыМы будем рассматривать 5 видов операторов программы надданным множествомпеременных. Некоторым из них приписанафункция:71.Начальный оператор START: y  f(x). Здесь f являетсяфункцией Dx  Dy+, инициализирующей промежуточныепеременные программы на основе значений ее входныхпеременных.2.Оператор присваивания ASSIGN: y  g(x, y). Здесь g является функцией Dx  Dy  Dy+, вычисляющей новые значения промежуточных переменных.3.Условный оператор TEST: t (x, y).

Здесь t является предикатом на множестве значений входных и промежуточныхпеременных программы.4.Оператор соединения JOIN.5.Оператор завершения HALT: z  h(x, y). Здесь h являетсяфункцией Dx  Dу  Dz+, устанавливающей значения выходных переменных программы.Графическое представление операторов показано на рисунке 1.START:y  f( x )y  g( x, y )Начальный операторОператор присваиванияHALT:z  h( x, y )Завершающий оператор…TFt( x, y )Условный операторОператор соединенияРисунок 1.

Графическое представление операторов блок-схемы8В программу могут входить несколько операторов одного и тогоже типа, помеченных одной и той же функцией. Поэтому дляобеспечения уникальности одинаковых операторов в рамках однойпрограммы, мы будем помечать каждый оператор уникальнойметкой i. Таким образом, каждый оператор программы состоит изметки оператора и тела оператора, принадлежащего к одному изпятивозможныхтипов.Множествометоквсехоператоровпрограммы P будет обозначаться как P.Блок-схемыВ качестве модели программы мы будем использовать блоксхемы. Блок-схемой называется тройка ( V, N, E ), гдеV – конечное множество переменных программы,N – конечное множество операторов блок-схемы,E  N  {T, F, }  N – конечное множество связок блок-схемы,помеченных символами T, F или .Заметим,чтоблок-схемасоответствуеториентированномуграфу, вершинами которого являются операторы программы, аребрами – ее связки.

При этом все ребра помечены одним из трехсимволов.Корректно-определенной блок-схемой мы будем называть блоксхему удовлетворяющую следующим требованиям:1. В блок-схеме присутствует ровно один начальный оператор ине менее одного завершающего оператора.92. Любой оператор находится на ориентированном пути отначальногооператоракнекоторомузавершающемуоператору.3. Число связок, выходящих из каждого оператора, и пометкиэтих связок соответствуют типу оператора:a. Изначальногооператоравыходитровно1дуга,помеченная символом .b.