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

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

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

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

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

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

/₂, /"), где lj = f (t_u …, t_n) — обозначение соответствующего преобразова ния, выполняемого оператором;

• 2) если i и j — вход и выход условной вершины, то дуге «i —> j» ставится в соответствие формула с контрольным предикатом Q, & Р —> Q, где Р = = P (t_1?…, t_n) — контрольный предикат;
• 3) узел Q_m объединяет два и более состояний Q, на входе операторной или условной вершины и записывается в виде тождества Q_m = XQ_;(?j, t₂, t_n),
• 4) начало программы Qq — нуль-местный предикат (простое высказывание);
• 5) конец программы — Q_k.

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

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

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

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

• 1) Qo —> Q (A, В, S = 0) & (В > 0) & (А > 0) (ввод данных);
• 2) Qi (A_t В, 0) -> Q₂(A, В, 0) (начало);
• 3) Q₂(A Л, S) = Q_X(A, Л, 0) v Q_S(A, Л, 5);
• 4) <2₂&(Я = 0)->О4(Л, Л, S);
• 5) Q₂ & (Л > 0) -> 0з (д, у, 2);
• 6) (2₅(Л, В — 1, 5 + Л);
• 7) СМА Л, S) -> (2б (Л, Л, 5) & (Л = 0).

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

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

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

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

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

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

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

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

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

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

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