Формальные методы (Formal methods) базируются на формальной спецификации программ. Данная тема анонсирована в сообщении:
http://forum.oberoncore.ru/viewtopic.php?f=140&t=5555#p93861. Цель темы -- дать краткое популярное изложение для всех, кто хотел бы получить представление о формальных методах, применяемых в программной инженерии. Материал будет изложен в виде набора коротких глав.
Глава 1. Формальные спецификации
Спецификация программы -- декларативное описание, определяющее программу в целом, в частности интерфейс программы с пользователем. Спецификация -- внешнее описание программы, абстрагированное от особенностей ее реализации.
Рассмотрим сначала
программы-функции, у которых взаимодействие с
окружением программы ограничивается вводом входных данных и выводом результатов вычисления; других взаимодействий с окружением нет.
Спецификация программы-функции состоит из предусловия и постусловия.
Предусловие -- набор условий, определяющих область входных данных.
Постусловие -- набор условий, определяющих связи между значениями входных данных и результатов. Спецификация определяет условие математической задачи, решением которой является программа-функция. Исходные переменные задачи соответствуют входным данным, а неизвестные переменные -- результатам программы.
В качестве примера, рассмотрим известную программу вычисления
наибольшего общего делителя чисел a и b:
Код:
loop {
if (a == b) return a;
if (a < b) b = b – a
else a = a – b
}
Спецификация программы представлена фразой "наибольший общий делитель". Делитель -- известное математическое понятие, и поэтому данная фраза вроде бы должна иметь строгий математический смысл. Однако при a = 0 и b = 1.5 программа не работает. Делитель, как известно, второй операнд в операции деления. Оказывается, нет. Здесь подразумевается совсем другое понятие делителя в смысле делимости нацело, причем это свойство определено только для целых чисел. Значит, что значение b = 1.5 не годится. Далее, делитель для a = 0 смысла не имеет.
Таким образом, содержательная формулировка спецификации в виде текста на русском языке может содержать различного рода неточности, которые потенциально могут привести к неверной программе. Чтобы избежать этого, необходимо использовать
формальные спецификации в виде набора
логических формул на одном из строгих
языков спецификаций. Таких языков много. Наиболее известные из них: VDM, Z, B.
Представим формальную спецификацию программы наибольшего общего делителя на некотором языке спецификаций, который определен здесь с учетом ограниченного алфавита допустимых литер в сообщениях Форума. В языке спецификаций используются следующие обозначения:
and -- конъюнкция,
=> -- импликация,
exists -- квантор существования,
forall -- квантор всеобщности.
Предусловие определяется формулой:
nat a, b and a > 0 and b > 0
Здесь описатель
nat определяет натуральный тип чисел; "
nat a, b" означает, что a и b -- натуральные числа. Формула в целом определяет, что a и b являются натуральными положительными числами.
Чтобы записать формулу для постусловия, необходимо сначала определить подформулу divisor(a, x) для условия "число x является делителем числа a":
divisor(a, x) = exists nat z > 0. x * z = a
Правая часть формулы определяет, что существует такое число z, которое при умножении на x дает a, т.е. число a делится на x без остатка.
На следующем шаге надо определить подформулу divisor2(a, b, x) для условия "число x является общем делителем для чисел a и b":
divisor2(a, b, x) = divisor(a, x) and divisor(b, x)
Наконец, записывается формула для постусловия gcd(a, b, c), определяющего, что число
c является общим делителем чисел a и b, причем этот делитель наибольший среди других возможных:
gcd(a, b, c) = divisor2(a, b, c) and forall x. (divisor2(a, b, x) => x ≤ c)
Формальные спецификации программ являются обязательными для всех видов формальных методов, проверяющих корректность программ относительно спецификаций применением различного вида инструментов доказательства теорем, представленных формулами на языке спецификаций.
Вход
FAQ
Поиск
