Lecture-Analytical Verification

ВведениеДанный   документ   содержит   краткий   конспект   лекций   по   “Аналитической  верификации   программ”,   прочитанных   в   рамках   курса   по   “Формальным   методам  спецификации  программ”  на  факультете  ВМиК  МГУ  им.  Ломоносова.Верификация  последовательных  программМы   начнем   рассмотрение   методов   верификации   с   простейших   моделей  последовательных   программ.   Первая   модель   будет   соответствовать   программам,  написанным  на  структурном  языке  программирования без  массивов без  использования  адресной  арифметики без  рекурсии  (вызова  подпрограмм) без  взаимодействия  с  окружением  (например,  посредством  операторов  ввода-вывода)Далее   мы   расширим   эту   модель   для   описания   последовательных   программ   с  массивами.Методы   верификации   рекурсивных   программ   будут   рассмотрены   на   следующей  лекции.Программы,   взаимодействующие   с   окружением,   относятся   к  параллельным   (или,   как  их  еще  называют,  реактивным)  программам  и  мы  их  обсудим  в  соответствующем  разделе.Для   программ,   использующих   адресную   арифметику,   нет   хороших   методов  верификации,   так   как,   создавая   модели   таких   программ,   нет   возможности  абстрагироваться   от   содержимого   памяти.

  Поэтому   размеры   получающихся   моделей   не  позволяют  применять  имеющиеся  методы  верификации.Методы  верификации  ФлойдаМатематическая  модель  программыОписание   математической   модели   мы   начнем   с   нескольких   вспомогательных  определений.Переменные  программыКаждая   программа   работает   с   конечным   числом   переменных.

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

  Выходные   переменные  содержат  значения,  вычисляемые  данной  программой.Каждая  переменная  v может  принимать  значения  из  некоторого  множества  Dv,  которое  называется  доменом переменной.  Также,  мы  будем  выделять  три  непустых  домена: входной  домен Dx = Dx1  Dx2  …   Dxa домен  программы Dy = Dy1  Dy2  …   Dyb выходной  домен Dz = Dz1  Dz2  …   DzcМножество  значений  всех  переменных  образует   универсальный  домен D.  Это  значит,  что  для   любой  переменной   v выполнено  соотношение:   Dv  D.

 Кроме  того,  мы  выделим  два   специальных   значения:   Т   (истина)   и   F   (ложь).   Функции,   принимающие   значение  только   из   множества   {   Т,   F }   мы   будем   называть   предикатами на   области   определения  функции.Расширенным   доменом Dv+ переменной   v будем   называть   домен   этой   переменной,  расширенный   специальным   значением    (Dv+ = Dv  {  }   ).   Значение    будет  использоваться  для  обозначения  не  инициализированного  значения  переменной.Операторы  программыМы   будем   рассматривать   5   видов   операторов   программы   над   данным   множеством    переменных:Начальный   оператор START: y  f( x ).   Здесь   f является   функцией   Dx  Dy,инициализирующей   промежуточные   переменные   программы   на   основе  значений  ее  входных  переменных.2.Оператор   присваивания ASSIGNMENT: 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.1.START:y  f( x )y  g( x, y )Начальный  операторОператор  присваивания…TFt( x, y )Условный  операторОператор  соединенияHALT:z  h( x, y )Завершающий  операторРисунок  1.  Графическое  представление  операторов блок-схемыДля   обеспечения   уникальности   одинаковых   операторов   в   рамках   одной   программы,  мы   будем   помечать каждый   оператор   уникальной   меткой   i.   Таким   образом,   каждый  оператор  программы  состоит  из  метки  оператора и  тела  оператора,  принадлежащего  к  одному  из  пяти  возможных  типов.

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

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

Из   начального   оператора   выходит   ровно   1   дуга,   помеченная   "пустым"  символом  .b. Из   оператора   присваивания   выходит   ровно   1   дуга,   помеченная   "пустым"  символом  .c. Из   условного   оператора   выходит   ровно   2   дуги,   причем   одна   из   них  помечена  символом  T,  а  другая  – символом  F.d.

Из   оператора   соединения   выходит   ровно   1   дуга,   помеченная   "пустым"  символом  .e. Из  завершающего  оператора  соединения  не  выходит  ни  одной  дуги.4. Число  связок  входящих  в  каждый  оператора  соответствует  его  типу:a. В  начальный  оператор  не  входит  ни  один  оператор.b. В  оператор  присваивания,  условный  и  завершающий  оператор  входит  ровно  одна  дуга.c. В  оператор  соединения  входит  более  или  равно  одной  дуги.Заметим,   что   для   каждого   оператора   n и   символа   s корректно-определенной   блоксхемы  P существует  не  более  одной  связки  (n, s, n' )  E.

 Если  такая  связка  существует,  то  оператор   n'  мы  будем   называть  последователем  оператора   n по  метке   s и  обозначать  как  succ(n,s).Далее   мы   будем   рассматривать   только   корректно-определенные   блок-схемы,   и,  поэтому,  слово  'корректно-определенная'  будет  опускаться.В   графическом   представлении   блок-схем   мы   будем   опускать   некоторые   детали.  Например,   ребра   помеченные   символом    будут   изображаться   без   соответствующей  метки.

  Как   правило,   будут   опускаться   метки   операторов   блок-схемы,   а   в   операторах  соединения  не  все  входящие  ребра  будут  изображаться  со  стрелками  на  конце.Для  определения  функций  будет  использоваться  следующая  нотация:( y1, y2,  …,  yb )  ( f1( x, y ), f2( x, y ),  …,  fb( x, y ) )Пример   графического   представления   блок-схем   можно   увидеть   на   рисунке   2,   где  представлена  блок-схема  программы  целочисленного  деления.

 В  этом  примере  множество  переменных   V = { x1, x2, y1, y2, z1, z2 }   состоит  из   двух   входных,   двух   промежуточных   и  двух  выходных  переменных.  Доменом  всех  переменных  является  множество  целых  чисел.Семантика  блок-схемКонфигурацией программы  P будем  называть  пару  (  ,  ),  где   P – метка  текущего  оператора  программы,  = ( d1, d2,   …,   da+b )  Dx+  Dy+ – вектор   значений   входных   и  промежуточных  переменных  программы.Если     Dx+  Dy+ – вектор   значений   входных   и   промежуточных   переменных  программы,  а  функция  f(  x, y ): Dx+  Dy+  Dy+ вычисляет  новые  значения  переменных  y,START:( y1, y2 )  ( 0, x1 )Ty2  x2( y1, y2 )  ( y1+1, y2- x2 )FHALT:( z1, z2 )  ( y1, y2 )Рисунок  2.

 Блок-схема  программы  целочисленного  делениято   вектор   значений   входных и   промежуточных   переменных   программы,   полученный  путем  замены  в   значений  переменных  y на  f(),  мы  будем  обозначать  как  [y  f(x, y)].Конечная   или   бесконечная   последовательность   конфигураций   {   Ci | i =   1,   …,   n,   …   }  программы  P называется  вычислением,  если1.

Метка  первой  конфигурации  программы  является  меткой  начального  оператора.2. Значения  всех  входных  переменных  программы  являются  определенными  ( )  и  неизменными  во  всех  конфигурациях  вычисления.3. Значения   промежуточных   переменных   в   первой   конфигурации   являются  неопределенными  (равными  ).4. Если   метка   i текущего   оператора   конфигурации   Ci является   меткой   начального  оператора   START: y  f( x ),   то   следующая   конфигурация   Ci+1 состоит  из   метки  оператора  succ( ni,  )  и  вектора  значений  переменных  i+1 = i[y  f( x )].5. Если   метка   i текущего   оператора   конфигурации   Ci является   меткой   оператора  присваивания   ASSIGNMENT: y  g( x, y ),   то   следующая   конфигурация   Ci+1состоит   из   метки   оператора   succ( ni,  )   и   вектора   значений   переменныхi+1 = i[y  g( x, y )].6. Если   метка   i текущего   оператора   конфигурации   Ci является   меткой   условного  оператора   TEST: t( x, y ) и   предикат   t( x, y ) при   значениях   переменных   iпринимает   значение   T,   то   следующая   конфигурация   Ci+1 состоит   из   метки  оператора  succ( ni, T )  и  вектора  значений  переменных  i+1 = i.7.