Технология программирования. - 42 стр.

UptoLike

Рубрика:

- 44 -

При статической проверке текст модуля просматривается на предмет выяв-

ления ошибок. Причём, ошибки, обнаруженные таким методом, рекомендуется ис-

правлять не сразу, а после «прочтения» всего модуля.

Сквозное прослеживание – вид динамического контроля. Группа программи-

стов вручную «прокручивает» выполнение модуля на некотором тестовом наборе.

Третий метод применяется пока очень редко.

9. Подтверждение правильности программ

Для повышения надёжности ПС их необходимо снабжать дополнительной ин-

формацией. Такая информация может быть задана в виде формализованных и не-

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

грамм. Такие утверждения называются обоснованиями программ [1]. Неформали-

зованные обоснования вводятся для объяснения мотива принятия решений, что

упрощает поиск и исправление ошибок.

Формализованные обоснования позволяют

доказать некоторые свойства программ как вручную, так и автоматически.

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

ние триад Хоора [1].

Пусть S – обобщённый оператор над информационной средой (ИС) IS, а P и Q

– предикаты (утверждения) над информационной средой IS. Тогда запись {P}S{Q}

называют триадой Хоора, в которой Р – предикат предусловия, а Q – предикат

постусловия относительно оператора S. Говорят, что оператор (или программа) S

обладает условием {P}S{Q}, если всякий раз перед его выполнением истинен пре-

дикат Р, а после его выполнения истинен предикат Q.

Примеры свойств программ:

{n = 0} n: = n + 1 {n = 1},

{n < m} n: = n+k {n < m + k},

{n < m + k} n: =3*n {n < 3*(m + k)},

{n > 0} p: = 1; m: = 1

ПОКА m <> n ДЕЛАТЬ

m: = m+1; p: = p*m

ВСЁ ПОКА

{p = n!}.