Применение логики к верификации алгоритмов

Предписывающие (вычислительные) алгоритмы могут быть представлены неформальным описанием в виде блок-схем. В этих формах алгоритмы легче поддаются анализу и верификации.

Проверка корректности неформального алгоритма может быть основана на логической модели алгоритма, исследования которой могут быть выполнены формальными логическими методами.

В программе выбираются контрольные точки, которым ставят в соответствие предикаты, обозначающие состояние программы.

Логическое описание семантики программы:

1) если i и j — это вход и выход операторной вершины, то переход из i в j — это дуга, которая определяется импликацией Qj(t^ t2, tn) —> Q;(/t,

/2, /„), где lj = f(tu ..., tn) обозначение соответствующего преобразова

ния, выполняемого оператором;

  • 2 ) если i и j — вход и выход условной вершины, то дуге «i —> ставится в соответствие формула с контрольным предикатом Q, & Р —> Q,, где Р = = P(t1?..., tn) контрольный предикат;
  • 3) узел Qm объединяет два и более состояний Q, на входе операторной или условной вершины и записывается в виде тождества Qm = XQ;(?j, t2,tn),
  • 4) начало программы Qq — нуль-местный предикат (простое высказывание);
  • 5) конец программы — Qk.

Для целого умножения используется очевидный простой алгоритм многократного суммирования S =ХА Для описания алгоритма используется блок-схема, в кото- в

рой А, В — целые числа; А — множимое; В — множитель; S — произведение, которое вычисляется по указанной формуле (рис. 5.2).

Схема алгоритма к примеру 5.3

Рис. 5.2. Схема алгоритма к примеру 5.3

Формулы, описывающие схему алгоритма, в которой выделены точки контроля состояния машины Qq, ..., QС):

  • 1) Qo —> Q(A, В, S = 0) & (В > 0) & (А > 0) (ввод данных);
  • 2) Qi(At В, 0) -> Q2(A, В, 0) (начало);
  • 3) Q2(A Л, S) = QX(A, Л, 0) v QS(A, Л, 5);
  • 4) <22&(Я = 0)->О4(Л, Л, S);
  • 5) Q2 & (Л > 0) -> 0з(д:, у, 2);
  • 6) <2з(Д Л, 5) -> (25(Л, В - 1, 5 + Л);
  • 7) СМА Л, S) -> (2б(Л, Л, 5) & (Л = 0).

Контрольные формулы-инварианты в алгоритме:

Интерпретация формул для конкретных исходных данных эквивалентна исполнению программы.

Задача анализа программы следующая: доказать, что при ограниченных исходных данных программа имеет завершение в состоянии 0$(А, В, S) & & (В = 0), т.е.

Исполнение программы состоит из следующих шагов:

1) подстановка (интерпретация) значений переменных после ввода данных в формулу:

  • 2) переход к следующей формуле, в которой условие импликации истинно, и запуск итерационного процесса интерпретации (Q = Т):
    • а) выполнение формул, пока 1 не равно Ff,
    • б) формулы можно упорядочить для ускорения итерации;
    • в) формулы можно интерпретировать параллельно.

Символическое тестирование и частичные вычисления используются

для не полностью определенных данных с целью тестирования алгоритма. В результате интерпретации при частично определенных данных будет получена формула, которая совпадает с исходным определением метода вычисления.

Зададимся множимым А = а и множителем В = 3.

Интерпретация алгоритма в логике предикатов:

Подтверждается исполнение формулы S - а • 3 = X = « + « + а.

В традиционном программировании используются контрольные формулы, в которых проверяется состояние данных в конкретных точках программы. В языках программирования (C++, Паскаль) используется оператор assert (логическая формула с предикатами), при интерпретации этой формулы формируется признак (^или 7), который позволяет контролировать возможные ошибки в исходных данных и вычислениях.

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >