Доказательство частичной правильности как часть процесса программирования

Все примеры доказательства правильности в этом учебном пособии относились к законченным и небольшим программам. Однако на практике такое доказательство должно проводиться программистом во время самого процесса программирования. Не следует ожидать, что кто-нибудь возьмет большую, закон­ченную программу и начнет доказывать ее правильность. Интеллектуальные затраты на такую работу были бы, вероятно, очень велики. Нужно доказывать правильность небольших фрагментов по мере того, как они составляются. Для того чтобы это можно было делать, такие секции (фрагменты) не должны вместе образовывать запутанный клубок, где не найдешь ни конца, ни начала каждой. Многие утверждают, что программист сможет избежать излишних необходимых усложнений и запутанных структур, если он не будет использовать переходы GO TO и ограничит себя небольшим множеством операторов управления с одним входом и одним выходом. Такими операторами могут быть: последовательное выполнение, условное выполнение (ветвление) вида IF С THEN SI ELSE S2 и итеративная конструкция основного вида WHILE С DO S. Программы, написанные в таком стиле, часто называют «структурирован­ными» программами. Тем не менее использование такого ограниченного подмножества операторов управления, конечно, не спасает программиста от всех «болезней». И с такими операторами управления, как и с оператором GO TO, можно написать «мрачную» программу, которую трудно понять и верифицировать. Важно, чтобы программа была ясна по замыслу и при этом не использовались такие операторы управления, которые запутывают связи между отдельными частями (путем переходов вперед или назад с использованием оператора GO TO).

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

Выполнение таких операторов будет приводить к справедли­вости некоторых постусловий (утверждений о правильности такой подчасти) при условии, что до выполнения были справедливы предусловия (входные утверждения для этой подчасти). Таким образом, доказывая правильность большого фрагмента, вовсе нет необходимости разбираться во всех его частях. Часто процесс идет в обратном порядке, т. е. про­граммист, работая по принципу «сверху вниз», составляет большой фрагмент, оставляя неопределенным в данный момент некоторые его части. Доказывая правильность этого фрагмента, он исходит из того, что упомянутые части будут написаны так, что их выполнение будет приводить к справед­ливости некоторых постусловий, если до их выполнения были справедливы предусловия. После этого, опираясь на эти утверждения, доказывается правильность большого фраг­мента. Позже, при составлении программ для более мелких частей, для доказательства их правильности нужно лишь показать, что из допущения справедливоети до их выполнения предусловий следует справедливость после выполнения постусловий.

Как уже говорилось в п. 2.5, мы не считаем, что программисту необходимо выписывать все пункты дока­зательства правильности. Однако он должен выписывать все ключевые утверждения (как примечания), а затем удосто­веряться в их справедливости (без деталей). Программист должен (без лишних подробностей) удостовериться и в том, что программа в конце концов закончит работу.

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