Неформальное обозначение обобщенного оператора на псевдокоде производится на естественном языке произвольным предложением, раскрывающим в общих чертах его содержание. Единственным формальным требованием к оформлению такого обозначения является следующее: это предложение должно занимать целиком одно или несколько графических (печатных) строк и завершаться точкой.
Для каждого неформального обобщенного оператора должно быть создано отдельное описание, выражающее логику его работы (детализирующее его содержание) с помощью композиции основных конструкций структурного программирования и других обобщенных операторов. В качестве заголовка такого описания должно быть неформальное обозначение детализируемого обобщенного оператора. Основные конструкции структурного программирования могут быть представлены в следующем виде (см. рис. 8.2). Здесь условие может быть либо явно задано на базовом языке программирования в качестве булевского выражения, либо неформально представлено на естественном языке некоторым фрагментом, раскрывающим в общих чертах смысл этого условия. В последнем случае должно быть создано отдельное описание, детализирующее это условие, с указанием в качестве заголовка обозначения этого условия (фрагмента на естественном языке).
| Следование: обобщенный_оператор обобщенный_оператор Разветвление: ЕСЛИ условие ТО обобщенный_оператор ИНАЧЕ обобщенный_оператор ВСЕ ЕСЛИ Повторение: ПОКА условие ДЕЛАТЬ обобщенный_оператор ВСЕ ПОКА |
Рис. 8.2. Основные конструкции структурного программирования на псевдокоде.
| Выход из повторения (цикла): ВЫЙТИ Выход из процедуры (функции): ВЕРНУТЬСЯ Переход на обработку исключительной ситуации: ВОЗБУДИТЬ имя_исключения |
Рис. 8.3. Частные случаи оператора перехода в качестве обобщенного оператора.
В качестве обобщенного оператора на псевдокоде можно использовать указанные выше частные случаи оператора перехода (см. рис. 8.3). Последовательность обработчиков исключительных ситуаций (исключений) задается в конце модуля или описания процедуры(функции). Каждый такой обработчик имеет вид:
ИСКЛЮЧЕНИЕ имя_исключения
обобщенный_оператор
ВСЕ ИСКЛЮЧЕНИЕ
Отличие обработчика исключительной ситуации от процедуры без параметров заключается в следующем: после выполнения процедуры управление возвращается к оператору, следующему за обращением к ней, а после выполнения исключения управление возвращается к оператору, следующему за обращением к модулю или процедуре (функции), в конце которого (которой) помещено данное исключение.
Рекомендуется на каждом шаге детализации создавать достаточно содержательное описание, но легко обозримое (наглядное), так чтобы оно размещалось на одной странице текста. Как правило, это означает, что такое описание должно быть композицией пяти-шести конструкций структурного программирования. Рекомендуется также вложенные конструкции располагать со смещением вправо на несколько позиций (см. рис. 8.4). В результате можно получить описание логики работы по наглядности вполне конкурентное с блок-схемами, но обладающее существенным преимуществом - сохраняется линейность описания.
| УДАЛЕНИЕ В ФАЙЛЕ ЗАПИСЕЙ ДО ПЕРВОЙ, УДОВЛЕТВОРЯЮЩЕЙ ЗАДАННОМУ ФИЛЬТРУ: УСТАНОВИТЬ НАЧАЛО ФАЙЛА. ПОКА НЕ КОНЕЦ ФАЙЛА ДЕЛАТЬ ПРОЧИТАТЬ ОЧЕРЕДНУЮ ЗАПИСЬ. ЕСЛИ ОЧЕРЕДНАЯ ЗАПИСЬ УДОВЛЕТВОРЯЕТ ФИЛЬТРУ ТО ВЫЙТИ ИНАЧЕ УДАЛИТЬ ОЧЕРЕДНУЮ ЗАПИСЬ ИЗ ФАЙЛА. ВСЕ ЕСЛИ ВСЕ ПОКА ЕСЛИ ЗАПИСИ НЕ УДАЛЕНЫ ТО НАПЕЧАТАТЬ "ЗАПИСИ НЕ УДАЛЕНЫ". ИНАЧЕ НАПЕЧАТАТЬ "УДАЛЕНО н ЗАПИСЕЙ". ВСЕ ЕСЛИ |
Рис. 8.4. Пример одного шага детализации на псевдокоде.
Идею пошаговой детализации приписывают иногда Дейкстре [8.1]. Однако Дейкстра предлагал принципиально отличающийся метод построения текста модуля [8.2], который нам представляется более глубоким и перспективным. Во-первых, вместе с уточнением операторов он предлагал постепенно (по шагам) уточнять (детализировать) и используемые структуры данных. Во-вторых, на каждом шаге он предлагал создавать некоторую виртуальную машину для детализации и в ее терминах производить детализацию всех уточняемых понятий, для которых эта машина позволяет это сделать. Таким образом, Дейкстра предлагал, по-существу, детализировать по горизонтальным слоям, что является перенесением его идеи о слоистых системах (см. лекцию 6) на уровень разработки модуля. Такой метод разработки модуля поддерживается в настоящее время пакетами языка АДА [8.7] и средствами объектно-ориентированного программирования [8.9].
8.4. Контроль программного модуля.
Применяются следующие методы контроля программного модуля:
статическая проверка текста модуля;
сквозное прослеживание;
доказательство свойств программного модуля.
При статической проверке текста модуля этот текст прочитывается с начала до конца с целью найти ошибки в модуле. Обычно для такой проверки привлекают, кроме разработчика модуля, еще одного или даже нескольких программистов. Рекомендуется ошибки, обнаруживаемые при такой проверке исправлять не сразу, а по завершению чтения текста модуля.
Сквозное прослеживание представляет собой один из видов динамического контроля модуля. В нем также участвуют несколько программистов, которые вручную прокручивают выполнение модуля (оператор за оператором в той последовательности, какая вытекает из логики работы модуля) на некотором наборе тестов.
Доказательству свойств программ посвящена следующая лекция. Здесь следует лишь отметить, что этот метод применяется пока очень редко.
Литература к лекции 8.
8.1. Г.Майерс. Надежность программного обеспечения. - М.: Мир, 1980. - С. 127-154.
8.2. Э.Дейкстра. Заметки по структурному программированию// У.Дал, Э.Дейкстра, К.Хоор. Структурное программирование. - М.: Мир, 1975. - С. 24-97.
8.3. Н.Вирт. Систематическое программирование. - М.: Мир, 1977. - С. 94-164.
Лекция 9. ДОКАЗАТЕЛЬСТВО СВОЙСТВ ПРОГРАММ
Понятие обоснования программ. Формализация свойств программ, триады Хоора. Правила для установления свойств оператора присваивания, условного и составного операторов. Правила для установления свойств оператора цикла, понятие инварианта цикла. Завершимость выполнения программы.
9.1. Обоснования программ. Формализация свойств программ.
Для повышения надежности программных средств весьма полезно снабжать программы дополнительной информацией, с использованием которой можно существенно повысить уровень контроля ПС. Такую информацию можно задавать в форме неформализованных или формализованных утверждений, привязываемых к различным фрагментам программ. Будем называть такие утверждения обоснованиями программы. Неформализованные обоснования программ могут, например, объяснять мотивы принятия тех или иных решений, что может существенно облегчить поиск и исправление ошибок, а также изучение программ при их сопровождении. Формализованные же обоснования позволяют доказывать некоторые свойства программ как вручную, так и контролировать (устанавливать) их автоматически.
Одной из используемых в настоящее время концепций формальных обоснований программ является использование так называемых триад Хоора. Пусть S - некоторый обобщенный оператор над информационной средой IS, P и Q - некоторые предикаты (утверждения) над этой средой. Тогда запись {P}S{Q} и называют триадой Хоора, в которой предикат P называют предусловием, а предикат Q - постусловием относительно оператора S. Говорят, что оператор (в частности, программа) S обладает свойством {P}S{Q}, если всякий раз, когда перед выполнением оператора S истинен предикат P, после выполнения этого оператора S будет истинен предикат Q.
Простые примеры свойств программ:
(9.1) {n=0} n:=n+1 {n=1},
(9.2) {n<m} n:=n+k {n<m+k},
(9.3) {n<m+k} n:=3*n {n<3*(m+k)},
(9.4) {n>0} p:=1; m:=1;
ПОКА m /= n ДЕЛАТЬ
m:=m+1; p:=p*m
ВСЕ ПОКА
{p=n!}.
Для доказательства свойства программы S используются свойства простых операторов языка программирования (мы здесь ограничимся пустым оператором и оператором присваивания) и свойствами управляющих конструкций (композиций), с помощью которых строится программа из простых операторов (мы здесь ограничимся тремя основными композициями структурного программирования, см. Лекцию 8). Эти свойства называют обычно правилами верификации программ.
9.2. Свойства простых операторов.
Для пустого оператора справедлива
Теорема 9.1. Пусть P - предикат над информационной средой. Тогда имеет место свойство {P}{P}.
Доказательство этой теоремы очевидно: пустой оператор не изменяет состояние информационной среды (в соответствии со своей семантикой), поэтому его предусловие сохраняет истинность и после его выполнения.
Для оператора присваивания справедлива
Теорема 9.2. Пусть информационная среда IS состоит из переменной X и остальной части информационной среды RIS:
IS = {X, RIS}.
Тогда имеет место свойство
{Q(F(X, RIS), RIS)} X:= F(X, RIS) {Q(X, RIS)} ,
где F(X, RIS) - некоторая однозначная функция, Q - предикат.
Доказательство. Пусть до выполнения оператора присваивания был истинен предикат Q(F(X0, RIS0), RIS0), где {X0, RIS0} - некоторое произвольное состояние информационной среды IS, тогда после выполнения оператора присваивания будет истинен предикат Q(X, RIS), так как X получит значение F(X0, RIS0), а состояние RIS не изменяется данным оператором присваивания, и, следовательно, после выполнения этого оператора присваивания в этом случае
Q(X, RIS)=Q(F(X0, RIS0), RIS0).
В силу произвольности выбора состояния информационной среды теорема доказана.
Примером свойства оператора присваивания может служит пример 9.1.
9.3. Свойства основных конструкций структурного программирования.