Спецификации программ, объединение спецификаций.

На самом деле любую программу на ЯВУ можно рассматривать как подпрограмму, поскольку у нее тоже могут быть входные и выходные параметры. Тогда можно говорить о спецификации всей программы, ее правильности и верификации. Вспомним еще раз о пошаговой детализации. Этот метод позволяет сконструировать программу из отдельных крупных шагов, каждый из которых может быть вызовом подпрограммы, а может быть разбит на более мелкие. При обсуждении пошаговой детализации в п. 2 мы говорили, что для каждого шага должно быть определено, что должно быть подано на вход и что получится на выходе, а сам шаг рассматривается сначала как ''черный ящик``. Теперь мы можем сказать, что для каждого шага должна быть задана спецификация. Затем, после написания подпрограммы для этого шага, нужно будет ее верифицировать.

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

Пусть f, f1 и f2 - подпрограммы, P, P1 и P2 - их предусловия, а Q, Q1 и Q2 - постусловия, соответствующие данным предусловиям. Предполагаем, что все предикаты и функции определены на одном и том же множестве M.

Аксиомы следствия.

a) Если R - предикат, который следует из Q, то подпрограмма f правильна относительно спецификации {P}f{R}.

b) Если R - предикат, из которого следует P,

то подпрограмма f правильна относительно спецификации {R}f{Q}.

Аксиома следования.

Если Q1→P2, то подпрограмма F=(f1; f2) (т.е. подпрограмма, полученная последовательным выполнением подпрограмм f1 и f2) правильна относительно спецификации {P1}F{Q2}.

Аксиома цикла.

a) Если, , то подпрограмма |F=(while S do f) является правильной относительно спецификации .

Аксиомы выбора.

a) Если , и , то подпрограмма F=(if S then f1 else f2) правильна относительно спецификации {R}F{Q1}.

b) Если и , то подпрограмма F=(if S then f) правильна относительно спецификации {R}F{Q}.

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

Остановимся на нескольких важных моментах в связи с верификацией подпрограмм.

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

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

3. Даже для относительно простого случая – использования целочисленных данных - существуют трудности. Например, могут возникнуть ошибки связанные с переполнением, а математические аксиомы целых чисел этого не учитывают. В таких случаях перед выполнением операций, которые могут вызвать подобные ошибки, должна производиться проверка данных на допустимость. Более подробно об этом при обсуждении защитного программирования.

4. Реальные языки программирования имеют встроенные структуры или операторы, которые усложняют верификацию. Например, оператор goto. Это еще один повод от него отказаться. Кроме того, изменение подпрограммами глобальных переменных (побочный эффект) также оказывает негативное влияние на верификацию. Эта сложность легко преодолевается путем написания подпрограмм с полными спецификациями.

5. Самым, пожалуй, слабым местом аксиоматического подхода к верификации является невозможность доказать или опровергнуть тот факт, что подпрограмма закончит свою работу за конечное число шагов. Эта сложность возникает, когда подпрограмма использует цикл или рекурсию. Для доказательства того, что цикл закончит свою работу, используют уже рассмотренный нами метод итераций или его частный случай - метод инварианта цикла. Часто такое доказательство сводится к отысканию некоторой числовой величины, которая ограничена снизу (или сверху) условием окончания цикла и на каждой итерации цикла уменьшается (или увеличивается). Аналогичную схему используют при доказательстве конечности рекурсивных подпрограмм.