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

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

    Определение. Условие, характеризующее множество всех начальных состояний, при которых запуск обязательно приведет к событию правильного завершения, причем система останется в конечном состоянии, удовлетворяющем заданному постусловию, называется «слабейшим предусловием, соответствующим этому постусловию».

    Если  программа обозначается через  S, а желаемое постусловие через R, то соответствующее слабейшее предусловие обозначим

wp(S,R).

    Если  начальное состояние удовлетворяет  wp(S,R), то конструкция обязательно обеспечит в конце концов истинность R. Поскольку wp(S,R) - слабейшее предусловие, то это означает, что если начальное состояние не удовлетворяет wp(S,R), то такой гарантии дать нельзя, т.е. ход событий может привести к завершению работы в конечном состоянии, не удовлетворяющем R, а может даже вообще помешать достижению какого бы то ни было конечного состояния.

    В объем случае, множество возможных  постусловий столь огромно, что  эта информация в табличной форме (т.е., в виде таблицы, где каждому  постусловию R соответствует запись, в которой содержится соответствующее предусловие wp(S,R)), оказалась бы совершенно необозримой, а, следовательно, бесполезной. Поэтому определение семантики той или иной конструкции всегда дается другим способом - в виде правила, описывающего, как для любого заданного постусловия R можно вывести слабейшее предусловие wp(S,R). Когда нужно получить описание семантики конструкции S, то, в сущности, речь идет о соответствующем этой конструкции преобразователе предикатов.

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

P → wp(S,R)

справедливо для всех состояний, где → - импликация. Требуя, чтобы утверждение «P → wp(S,R)» было справедливо для всех состояний, мы тем самым требуем, чтобы всякий раз, когда P - истина, условие wp(S,R) тоже было истинным, тогда P - достаточное предусловие.

    Смысл wp(S,R), т.е. «слабейшего предусловия для начального состояния, при котором запуск обязательно приведет к событию правильного завершения, причем система S останется в конечном состоянии, удовлетворяющем постусловию R», позволяет установить, что преобразователь предикатов, рассматриваемый как функция от постусловия R, обладает рядом определенных свойств, сформулированных Э.Дейкстрой.

    Свойство 1. Для любой конструкции S

wp(S,"false") = false.

Свойство 1 известно также под названием  «свойства исключенного чуда».

    Свойство 2. Для любой конструкции S и любых постусловий Q и R, таких, что Q → R для всех состояний, справедливо также отношение

wp(S,Q) → wp(S,R)

для всех состояний.

    Свойство 3. Для любой конструкции S и любых постусловий справедливо

(wp(S,Q) and wp(S,R)) = wp(S,Q and R).

    Свойство 4. Для любой конструкции S и любых постусловий Q и R справедливо

(wp(S,Q) or wp(S,R)) → wp(S,Q or R)

для всех состояний.

    Свойство 4’. Для любой детерминированной конструкции S и любых постусловий Q и R справедливо

(wp(S,Q) or wp(S,R)) = wp(S,Q or R).

    Для формального описания семантики  конструкции S вводится язык разработки алгоритмов. Введение особого языка разработки алгоритмов обусловлено следующими причинами: во-первых, этот язык предназначен для описания преобразования предикатов, а не каких-либо данных, что отличает его от других языков; во-вторых, он является более общим по отношению к остальным алгоритмическим языкам программирования, поэтому, как следствие, его конструкции можно реализовать на любом языке; и в-третьих, программу, записанную на данном языке, легко исследовать на предмет ее корректности.

Формальный  язык описания логики программ

    Для описания логики работы программы рядом  ученых было предложено использовать формальный язык разработки алгоритмов (ЯРА).

    ЯРА строится по образцу универсальных  языков программирования типа Алгол  или PL/1 и состоит из двух частей: заданного набора операторов, построенных  по образцу языков программирования (внешний синтаксис), и общего, обычно неопределяемого внутреннего синтаксиса, пригодного для описания структур данных и процедур по их обработке в данной предметной области.

    В результате такого состава ЯРА по сравнению со стандартными блок-схемами  имеет ряд преимуществ:

• алгоритм, написанный на ЯРА, достаточно легко трансформируется в программу на одном из традиционных языков программирования;
• в ЯРА хорошо продуманы локализация и спецификация переменных;
• алгоритм, написанный на ЯРА, может быть верифицирован, т.е. может быть строго доказана его корректность.

Оператор  присваивания

    Если  переменная x должна быть заменена выражением (E), то синтаксис оператора присваивания выглядит следующим образом:

x := E, 

где x - идентификатор,

      E - выражение, составленное из идентификаторов и натуральных чисел при помощи символов и арифметических действий.

    При присваивании вычисляется значение E с использованием старого значения x, а затем содержимое x заменяется на вычисленное значение. Старое значение x при этом пропадает. Например, x:=x+1; увеличивает значение x на 1. Такая интерпретация присваивания элементарно описывается и логически.

    Обозначим через R_E→x результат преобразования при замене в предикате R всех вхождений переменной x некоторым выражением (E). Рассмотрим для заданных x и E такую конструкцию, чтобы для любых постусловий R получалось wp(S,R) = R_E→x; здесь x - координатная переменная нашего пространства состояний, а E - выражение соответствующего типа.

    Сказанное можно суммировать, определив:

wp("x := E",R) = R_E→x, для любого постусловия R.

    Данное  выражение можно рассматривать  как семантическое определение  оператора присваивания для любой  координатной переменной x и любого выражения E соответствующего типа.

Оператор  ветвления по условию.

    В общем случае синтаксис оператора  ветвления по условию определяется следующим образом:

if B₁ → SL₁ □ B₂ → SL₂ □ ... □ B_n → SL_n endif

где  B_i - логические выражения, называемые предохранителями;

      SL_i - список операторов, выполняемый в случае истинности значения соответствующего предохранителя.

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

    В классическом изложении Э.Дейкстры оператор ветвления по условию обладает тремя свойствами:

    1. Предполагается, что все предохранители  определены: если это не так,  т.е. процесс вычисления какого-то  предохранителя может привести  к работе без предварительного завершения, то допускается, что и вся конструкция не сможет правильно завершиться.

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

    3. Если начальное состояние таково, что ни один из предохранителей  не является истинным, то здесь  встречаемся с начальным состоянием, для которого не подходит ни  один из вариантов, и, следовательно,  вся конструкция в целом. Запуск  при таком начальном состоянии  приведет к отказу.

    Поскольку программы, реализующие криптографические  преобразования не могут и не должны обладать этими указанными свойствами, то для практического применения предлагается применять следующие  правила построения конструкций  условного ветвления, которые нейтрализуют указанные свойства:

    1. Поскольку реальная программа, полученная из разработанного алгоритма останавливаться не должна, то возможны два выхода: либо выбирать охраны таким образом, чтобы по крайне мере одна из охран имела бы значение "true" для любого набора переменных, от которых зависит значение охран, либо, если это не удастся сделать, дополнить оператор условного ветвления еще одной охраняемой командой

B_n+1 → SL_n+1,

где B_n+1 является отрицанием по отношению ко всем остальным охранам, а SL_n+1 является оператором пропустить Дейкстры. (Для оператора пропустить в языках низкого уровня есть аналог - команда NOP).

    2. Для устранения недетерминированности  оператор условного ветвления  обобщенного вида можно равносильно  заменить на следующую последовательность вложенных друг в друга операторов условного ветвления:

      if B₁ → SL₁

      □ non B₁ → if B₂ → SL₂

      non B₂ → …

      if B_n → SL_n

                                    non B_n → <пропустить>

                                    endif

                  endif

      endif

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

    Покажем, что данная конструкция оператора  условного ветвления охватывает и тот случай, когда для исключения останова программы в состав оператора  вводится дополнительная охраняемая команда, у которой охрана B_n+1 есть отрицание всех охран, а список операторов состоит из команды “пропустить”.

    По  определению 

    B_n+1 = non BB,

    B_n+1 = non (B₁ or B₂ or ... or B_n ),      (1)

т.е. чтобы  выполнился оператор пропустить, должно выполняться условие (1). С другой стороны, в композиции операторов ветвления, которая заменяет обобщенную форму  оператора условного ветвления  в алгоритме, оператор пропустить выполняется, если

non B₁ and non B₂ and ... and non B_n,

что по закону де Моргана эквивалентно (1).

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