Lecture-Analytical Verification, страница 2

Если   метка   i текущего   оператора   конфигурации   Ci является   меткой   условного  оператора   TEST: t( x, y ) и   предикат   t( x, y ) при   значениях   переменных   iпринимает   значение   F,   то   следующая   конфигурация   Ci+1 состоит   из   метки  оператора  succ( ni, F )  и  вектора  значений  переменных  i+1 = i.8. Если   метка   i текущего   оператора   конфигурации   Ci является   меткой   оператора  соединения   JOIN,   то   следующая   конфигурация   Ci+1 состоит   из   метки   оператора  succ( ni,  )  и  вектора  значений  переменных  i+1 = i.9. Если  метка  i текущего  оператора  конфигурации  Ci является  меткой  завершающего  оператора   HALT: z  h( x, y ),   то   Ci является   последней   конфигурацией  вычисления.Лемма   1.

Для   каждой   блок-схемы   P и   вектора   значений   ее   входных   переменных   xсуществует   единственное   вычисление,   в   первой   конфигурации   которого   значения  входных  переменных  равны  x.Каждой  блок-схеме  P мы  поставим  в  соответствие  функцию  M[P],  из  входного  домена  блок-схемы  в  выходной  домен,  расширенный  специальным  значением   ( M[P]: Dx  Dz+,где  Dz+ = Dz  {  }  ).  Если  вычисление  блок-схемы  P на  векторе  входных  переменных  xявляется   конечным,   то   функция   M[P](x)   принимает   значение   h( x, yn ), h - функция  завершающего   оператора,   последней   конфигурации   вычисления,   а   yn – вектор   значений  промежуточных   переменных   из   последней   конфигурации   вычисления.

  Если   вычисление  блок-схемы   P на   векторе   входных   переменных   x является   бесконечным,   то   функция  M[P](x)  принимает  значение  .Математическая  модель  требованийМатематическую   модель   требований   к   верифицируемой   программе   мы   будем  называть   спецификацией программы.   Семантика   спецификации   состоит   в   формальном  описании  требований  к  поведению  программы.Требований   к   поведению   программ   может   быть   огромное   множество,   но   в   данном  разделе   мы   будем   рассматривать   только  требования   к   функциональности  программ.   Под  требованиями   к   функциональности   понимаются   ограничения   на   результат   вычисления  программы  в  зависимости  от  значений  ее  входных  данных.СпецификацииСпецификацией   программы  над  переменными  V мы  будем  называть  два  предиката: входной  предикат  : Dx  {  Т,  F } выходной  предикат  : Dx  Dz  {  Т,  F }Выходной   предикат (или   постусловие)   определяет   какие   значения   выходных  переменных   программы   являются   корректными   относительно   значений   входных  переменных.

  А   входной   предикат (или   предусловие)   определяет   при   каких   значениях  входных   переменных   требуется   выполнение   ограничений   описанных   в   выходном  предикате.Задача  верификацииКорректность  программПусть  программа  задана  своей  моделью  в  виде  блок-схемы  P,  а  ее  спецификация   –предикатами   и  .  Мы  будем  говорить,  что программа   P частично   корректна относительно    и   ,   если   для   любого   вектора  значений  входных  переменных  ,  такого  что  ()  и  M[P]()   выполнено  ограничение  ( , M[P]()   ).   Частичную   корректность   программы   P относительно    и    мы   будем  обозначать  {}P{}. программа   P полностью   корректна относительно    и   ,   если   для   любого   вектора  значений  входных  переменных  ,  такого  что  ()  выполнены  ограничения  M[P]()  и   ( , M[P]()   ).

  Полную   корректность   программы   P относительно    и    мы   будем  обозначать  P.Заметим,  что  полная  корректность  P программы  относительно  входного  предиката     и  выходного   предиката   T эквивалентна   тому,   что   программа   P завершается   всегда,   когда  вектор  значений  входных  переменных  удовлетворяет  .  В  этом  случае  мы  будем  говорить,  что  P завершается на  .Лемма  2.

Пусть  даны  программа P и  спецификация  = ( ,  ). В  этом  случае  Pтогда  и  только  тогда,  когда  {}P{} и  PT.Исходя   из   данной   леммы,   для   доказательства   полной   корректности   программы  достаточно  доказать  ее  частичную  корректность  и  завершаемость.Из  определения  корректности  также  следует,  что  и  частичная,  и  полная  корректность  сохраняется   при замене   входного   предиката   на   более   сильный   и   выходного   на   более  слабый.  Таким  образом,  верна  следующая  лемма:Лемма   3. Пусть   дана   программа P. Пусть   предикаты , ',  и ' таковы,   что  формулы '   и   ' истинны.  Тогда   из  {}P{} следует  {'}P{} и  {}P{'}, из  P следует  'P и  P'.Следующая   лемма   позволяет   по   нескольким   утверждениям   о   частичной   и   полной  корректности  получать  новые  утверждения:Лемма  4. Пусть  дана  программа P.

Для  любых  программы P и  предикатов , 1 и 2выполнены  следующие  утверждения: из  {}P{1} и  {}P{2} следует  {}P{1  2}, из  P1 и  P2 следует  P1  2.Верификация  программы  целочисленного  деленияВ   дальнейшем,   мы   сформулируем   методы   доказательства   тотальной   корректности  программ  в  общем  случае,  но  сначала  обратимся  к  примеру.Для   этого   вернемся   к   программе   целочисленного   деления,   блок-схема   которой    представлена   на   рисунке   2.

  Мы   докажем   ее   полную   корректность   относительно  спецификации,  заданной  следующими  предикатами:  (x1  0)  (x2 > 0)  (x1 = z1x2 + z2)  (0  z2 < x2)Входной   предикат   спецификации   утверждает,   что   нас   будет   интересовать   поведение  программы   только   на   неотрицательных   значениях   переменной   x1 и   положительных  значениях   переменной   x2.   Выходной   предикат   определяет,   что   значения   выходных  переменных   программы   должно   удовлетворять   определению   целочисленного   деления   с  остатком.Доказательство   полной   корректности   будет   разбито   на   два   этапа.

  Сначала   мы  докажем,  что  программа  является  частично  корректной  относительно  входного  предиката    0  (x1  0)  (x2  0)   и   выходного   предиката   .   А   затем   мы   докажем   завершаемость  программы  на  .  Из  этого,  по  леммам  2  и  3,  будет  следовать  требуемое  утверждение.Заметим,   что   входной   предикат   0,   используемый   при   доказательстве   частичной  корректности,  является  более  слабым,  чем  . Это  связано  с  тем,  что  при  значении  входной  переменной  x2 равном  0,  программа  является  частично  корректной,  но  не  завершается.Частичная   корректность.

Поставим   в   соответствие   начальному   оператору   блоксхемы   входной   предикат   0,   завершающему   оператору   – выходной   предикат   ,   а   ребру  между   оператором   соединения   и   условным   оператором   – промежуточный   предикат   p,  задаваемый  формулой  p(  x1, x2, y1, y2 )  (x1 = y1x2 + y2)  (y2  0).  Это  ребро  на  рисунке  3  обозначено  буквой  B.1.   Рассмотрим   путь   от   начального   оператора   программы   до   ребра   B.   После  выполнения  начального  оператора  переменные  принимают  следующие  значения:x1x2y1y2x1x20x1Таким образом,  p(  x1, x2, y1, y2 )  (x1 = y1x2 + y2)  (y2  0)  (x1 = 0x2 + x1)  (x1  0) (x1  0).   А   последнее   неравенство   является   истинным   в   предположении,   что   выполнено  предусловие  программы  0  (x1  0)  (x2  0).

 То  есть:  0  (x1  0).A: 0( x1, x2 )  (x1  0)  (x2  0)START:( y1, y2 )  ( 0, x1 )p( x1, x2, y1, y2 ) (x1 = y1x2 + y2)  (y2  0)BTDy2  x2( y1, y2 )  ( y1+1, y2- x2 )FEHALT:( z1, z2 )  ( y1, y2 )С:  ( x1, x2, z1, z2 )  (x1 = z1x2 + z2)  (0  z2 < x2)Рисунок 3.  Программа  целочисленного  деления  и  ее  предикаты2.  Предположим,  что  предикат  p истинен  в  точке  B и  рассмотрим  путь  B-D-B.После  выполнения  условного  оператора  значения  переменных  не  изменяются,  то  есть  в   точке   D предикат   p также   будет   истинен,   а   так   как   в   точке   D лежит   на   ребре,  помеченном  символом  T,  то  в  точке  D будет  истинно  следующее  утверждение:(x1 = y1x2 + y2)  (y2  0)  (y2  x2)Докажем,   что   после   выполнения   последующего   оператора   присваивания   предикат   pтакже  будет  истинен:D: (x1  y1x2 + y2)  (y2  0)  (y2  x2)B: p( x1, x2, y1 + 1, y2  x2 )  (x1  (y1+1)x2 + y2  x2)  (y2  x2  0)(x1  y1x2 + y2)  (y2  0)  (y2  x2)  (x1  (y1+1)x2 + y2  x2)  (y2  x2  0)(x1  y1x2 + y2)  (y2  0)  (y2  x2)  (x1  y1x2 + y2)  (y2  x2  0)T3.

  И   в   завершении,   рассмотрим   последний   путь:   от   точки   B до   завершающего  оператора.Предположим,   что   в   точке   B истинен   предикат   p.   Тогда   при   попадании   в   точку   Eбудет  истинно  следующее  утверждение:(x1 = y1x2 + y2)  (y2  0)  (y2 < x2)Докажем,  что  после  завершающего  оператора  будет  истинен  выходной предикат  :E: (x1 = y1x2 + y2)  (y2  0)  (y2 < x2)C: ( x1, x2, y1, y2 )  (x1 = y1x2 + y2)  (0  y2 < x2)(x1 = y1x2 + y2)  (y2  0)  (y2 < x2)  (x1 = y1x2 + y2)  (0  y2 < x2)TИз  рассмотренных  свойств  программы  следует,  что  для  любого  конечного  вычисления  программы   целочисленного   деления   при   значениях   входных   переменных  удовлетворяющих   предусловию,   значения   выходных   переменных   будут   удовлетворять  постусловию.

  Или   другими   словами,   программа   целочисленного   деления   является  частично  корректной  относительно  спецификации  0 = ( 0,  ).A: ( x1, x2 )  (x1  0)  (x2  0)START:( y1, y2 )  ( 0, x1 )q( x1, x2, y1, y2 )  (y2  0)  (x2  0)u(x1, x2, y1, y2)  y2BTDy2  x2( y1, y2 )  ( y1+1, y2- x2 )FHALT:( z1, z2 )  ( y1, y2 )Рисунок  4.

 Доказательство  завершимости  программы   целочисленного  деленияЗавершаемость. До   сих   пор,   мы   доказали   корректность   программы   только   условно.  Мы   доказали,   что   если   программа   завершается,   то   ее   результат   удовлетворяет  предъявляемым   к   нему   требованиям.   Теперь   докажем,   что   программа   целочисленного  деления   действительно   завершается   при   значениях   входных   переменных  удовлетворяющих  входному  предикату  .Рассмотрим   блок-схему   программы   целочисленного   деления   (рисунок   4).

  Во   время  доказательства   частичной   корректности   программы,   мы   доказали,   что   если   значения  входных   переменных   удовлетворяют   предикату   0,   то   при   всяком   прохождении   точки   Bзначения   входных   и   промежуточных   переменных   будут   удовлетворять   следующему  условию:   (x1 = y1x2 + y2)  (y2  0).   Из   этого   следует,   что   если   значения   входных  переменных   удовлетворяют   более   сильному   предикату   ,   то   при   всяком   прохождении  точки   B значение   промежуточной   переменной   y2 будет   неотрицательным.   С   другой  стороны,   значения   входных   переменных   не   изменяются   в   ходе   выполнения   программы,  поэтому  предикат    является  истинным  в  любой  промежуточной  точке.  Отсюда  следует,  что  в  точке  B будет  выполнено  следующее  условие:  (y2  0)  (x2  0).Рассмотрим   цикл   B-D-B.