Основные подходы к обеспечению качества программного обеспечения

if B → SL₁ □ non B → SL₂ endif,

где один из операторов SL_i может состоять из оператора пропустить. Поскольку оператор условного ветвления состоит из элементарных операторов условного ветвления, то для его исследования достаточно провести анализ элементарного оператора условного ветвления.

    Рассмотрим  охраны оператора элементарного  условного ветвления. Очевидно, что  ситуация, когда у оператора подобного  типа BB = "false" невозможна, поскольку

BB = B or non B = "true"

по определению  оператора элементарного условного  ветвления. Из этого следует, что  в алгоритме, операторы условного  ветвления которого можно разложить  на операторы элементарного условного  ветвления, невозможна ситуация останова.

    Другим  свойством оператора элементарного  условного ветвления, вытекающим из его структуры, является то, что при  входе в этот оператор достаточно вычислить значение только одной  из двух охран, поскольку вторая является отрицанием первой. Это свойство полезно  для преобразования алгоритма в  программу на языке низкого уровня.

Оператор  цикла.

    Синтаксическая  запись обобщенного оператора цикла  определяется следующим образом:

while B₁ → SL₁ □ B₂ → SL₂ □ ... □ B_n → SL_n endwhile

    Неформальное  описание новой определяемой конструкции, называемой while-endwhile таково: после запуска проверяются все предохранители. Если нет ни одного истинного значения предохранителя, то работа завершается. Если же имеются предохранители с истинными значениями, то один из соответствующих списков операторов запускается, а после его завершения реализация снова начинает общую проверку всех предохранителей. Отметим, что после срабатывания оператора некоторые предохранители, бывшие ложными, могут стать истинными (и наоборот).

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

    Очевидно, что такой конструкцией цикла  является цикл с одним охраняемым списком операторов:

while B → SL endwhile.

    Если  значение B истинно всегда, тело цикла SL повторяется бесконечно и цикл никогда не завершится. Следовательно, результат выполнения цикла с условием продолжения определен, если:

• значение условия B определено (истинно или ложно) при каждом его вычислении,
• результат каждого выполнения тела цикла S определен,
• значение условия B оказывается ложным после конечного числа выполнений тела цикла S.

Доказательство  корректности алгоритма

    Для доказательства корректности программы, записанной на формальном языке, (верификация) формулируется математическая теорема  Q {S} R, которая затем доказывается. Доказательство теоремы о корректности принято разбивать на две части. Одна часть служит для доказательства того, что рассматриваемый алгоритм вообще может завершить работу (проводится анализ всех циклов). В другой части доказывается корректность постусловия в предположении, что алгоритм завершает работу.

    Чтобы понять как происходит доказательство корректности, рассмотрим небольшой пример.

    Пусть необходимо проверить правильность утверждения:

{10<y<x+N and 0≤x<13} x := x-5 {10<y and x<8}

Здесь отметитим, что форма записи a≤b<c не что иное, как сокращенная запись выражения (a≤b and b<c). Поэтому приведенное утверждение эквивалентно следующему:

{10<y and y<x+N and 0≤x and x<13} x := x-5 {10<y and x<8}

      Для того, чтобы получить предусловие оператора присваивания относительно его постусловия, заменим в постусловии переменную x на выражение, задаваемое оператором присваивания, т.е. на x-5. После выполнения данного шага надо показать, что

{10<y and y<x+N and 0≤x and x<13} → {10<y and x-5<8}.

Данное  выражение эквивалентно следующему выражению

{10<y and y<x+N and 0≤x and x<13} → {10<y and x<13},

в котором заданное предусловие (левая часть импликации) сильнее полученного предусловия (правая часть импликации). Т.о. полученная импликация является истинной, а значит наш алгоритм, состоящий из одного оператора присваивания, корректен относительно заданных пред- и постусловий.■

      Будем надеется, что тривиальность данного примера никого не ввела в заблуждение. Доказательство корректности более сложных программ, содержащих циклы и операторы условного ветвления, существенно превосходит по сложности доказательство корректности одного оператора присваивания.

      С другой стороны, может возникнуть вопрос, а зачем вообще использовать доказательство корректности алгоритмов и программ, если они настолько трудоемки  и требуют соответствующей подготовки? Нельзя ли обойтись простыми тестовыми  примерами? Частично ответ на эти  вопросы был дан в начале главы. Дополнить его можно следующими рассуждениями. Допустим, некто программирует произвольный криптографический алгоритм, для которого есть набор тестовых примеров. Программа может быть составлена таким образом, чтобы при подаче на вход программы «тестового примера № 1» на выходе был подан «правильный ответ №1», при подаче «тестового примера №2» на выход был подан «правильный ответ №2» и т.д., а при подаче произвольного набора данных, на выход подавался бы случайный «вроде бы похожий на правильный» ответ. К сожалению, приведенный случай не является гипотетическим и может быть проиллюстрирован рядом примеров из практики. 

    Литература

1. В.В.Липаев. Программно–технологическая безопасность информационных систем. Информационный бюллетень Jet Info № 6/7, 1997.
2. Э.Дейкстра. Дисциплина программирования: Пер. с англ. – М.:Мир, 1978.
3. Бейбер Р.Л. Программное обеспечение без ошибок: Пер. с англ. / Под ред. Д.И.Правикова. – М.: Джон Уайли энд Санз, Радио и связь, 1996.
4. Семьянов П.В. Почему криптосистемы ненадежны? Тезисы доклада на конф. «Методы и технические средства обеспечения безопасности информации», СПбГТУ, 1996.