Игошин Математическая логика и теория алгоритмов (1019110), страница 98
Текст из файла (страница 98)
Пусть а — программа, Р— утверждение, относящееся к входным данным, которое должно быть истинно перед выполнением программы а (оно называется предусловием программы а), Д— утверждение, которое должно быль истинно после выполнения программы а (оно называется постусловием программы а). Различают два вида правильности программ: частичную и тотальную (полную). Программа а называется частично провильной относительно пред- условия Р и постусловия Д, если всякий раз, когда перед выполнением а предусловие Р истинно для входных значений переменных и а завершает работу, постусловие Д также будет истинно лля выходных значений переменных.
В этом случае будем использовать запись Р [аЯ. Программа а называется тотольно правильной относительно Р и Ц, если она частично правильна относительно Р и Ц и а обязательно завершает свою работу для входных значений переменных, удовлетворяющих условию Р. В этом случае пишем Р[а!] 9 Обратим внимание на то, что понятие правильности программы а сформулировано относительно соответствующих утверждений (условий) Р и ('!. Поэтому из истинности утверждения Р[а]Ц (или Р[а!] Ц соответственно) не обязательно следует истинность утверждения о правильности программы при других пред- и постусловиях. Аналогичным образом, замена в Р[а] Д (или Р[а!] Д) программы а на программу ]), вообще говоря, не сохраняет истинностного значения утверждения о правильности.
Не следует также думать, что при данных условиях Р и Ц существует только одна программа а, для которой высказывание Р[а] Д (или Р[а]] (г) истинно. Говорить о правильности программы самой по себе бессмысленно. Программа пишется с целью решения той или иной конкретной задачи. Каждая правильно поставленная задача содержит в себе условие (то, что дано) и вопрос, на который нужно дать ответ. При составлении программы условие задачи превращается в предусловие, а вопрос преобразуется в постусловие, имеющее 394 уже форму не вопроса, а утверждения, которое должно быть истинно всякий раз, когда ответ на вопрос задачи правилен.
Из определений следует, что всякая тотально правильная программа является частично правильной при тех же пред- и постусловиях. Обратное конечно же неверно. Ясно, что тотальная правильность «лучше» частичной, хотя доказать тотальную правильность программы, по-видимому, сложнее, чем частичную. Для доказательства частичной правильности операторных программ обычно используются различные модификации метода Флойда, который состоит в следующем.
На схеме программы выбираются контрольные точки так, чтобы любой циклический путь проходил по крайней мере через одну точку. С каждой контрольной точкой ассоциируется специальное условие (индуктивное утверждение или инвариант цикла), которое истинно при каждом переходе через эту точку. С входом и выходом схемы также ассоциируются пред- и постусловия. Затем каждому пути программы между двумя соседними контрольными точками сопоставляется так называемое условие правильности. Выполнимость всех условий правильности гарантирует частичную правильность программы. Один из способов доказательства завершения работы программы состоит во введении в программу дополнительных счетчиков для каждого цикла и в доказательстве их ограниченности в процессе доказательства частичной правильности программы. Одна из модификаций метода Флойда заключается в построении конечной аксиоматической системы (так называемой «логики Хоара»), состоящей из схем аксиом и правил вывода, в которой в качестве теорем выводимы утверждения о частичной правильности программ, в частности на языке программирования Паскаль.
Такая система используется и для задания аксиоматической семантики языка Паскаль. Аксиоматические системы, родственные логике Хоара, разработаны и для других алгоритмических языков программирования. Для доказательства правильности рекурсивных программ используется метод математической индукции, связанный с определением наименьшей неподвижной точки, а для программ со сложными структурами данных (например, графами, деревьями) — индукция по структуре данных. При этом в теоретических исследованиях ло логике Хоара рассматриваются обычные свойства аксиоматизаций в логике — их непротиворечивость и полнота. Пример 38.1. Рассмотрим простой пример программы и проанализируем ее на правильность.
Требуется составить программу, которая для любых натуральных х и у давала бы ответ на вопрос, делится ли х на у. Будем писать «у ~х» вместо «х делится на у», Тогда определение делимости можно записать следующим образом: (~гх е У)(Фу е Аг)[у)х е-у (Эп е Аг)(лу= х)).
395 Что должен делать компьютер, чтобы выяснить, существует ли такое и, что лу = х? Заменим последнее условие на следующее х = = у+ у+ ... + у (п слагаемых), которое, в свою очередь, равносильно следующему: 0 = х — у — у — ... — у (и вычитаемых). Проверка этого условия уже под силу компьютеру: нужно организовать цикл, который на каждом шаге вычитает сначала из х число у, затем из результата снова у, и так до тех пор, пока не получится число 0 или отрицательное число. В первом случае ответ на вопрос о делимости х на у будет положительным, во втором — отрицательным. Структурная схема программы, реализующей указанный алгоритм, представлена ниже, Итак, условие, налагаемое на входные данные: х в Ф, у в Ф; условие, которое необходимо проверить: г = О.
Докажем правильность этой структурной схемы и соответствующей программы методом от противного. Суть этого метода состоит в следующем. Допустим, что требуется доказать утверждение А. Мы принимаем гипотезу о том, что А ложно, т.е. истинно А. Если из А удается вывести противоречие В л ~В, то заключаем, что 4 на самом деле ложно (поскольку влечет противоречие). Значит, истинно А. В случае с рассматриваемой программой мы хотим доказать, что выдача нашей программой результата г = 0 действительно будет происходить в том и только в том случае, когда х делится на у. Это значит, что доказываемое утверждение А имеет вид: «в = 0 <-> ~-~ у ~ х», Допустим, что это утверждение неверно. Это означает„что ложна одна из импликаций г = 0 — » у~х» или «у~х — » г = 0», Предположим сначала, что ложна первая импликация «г = 0 -«у~х», т.е.
г = 0 истинно, но х на у не делится. В соответствии со структурной схемой г = 0 либо когда х = О, либо когда в процессе вычитания х — у-у...— у на некотором шаге получится О. В первом случае х делится на у в противоречие с допущением. То же происходит и во втором случае. Если х- у — у... — у= О, то х — лу= О, т е. х = лу для некоторого п, что и означает делимость х на у. Допустим теперь, что ложна вторая импликация, т.е.
что х делится на у, но г ~ О. Неравенство г ~ 0 может иметь место в одном из 396 следующих трех случаев: а) при невыполнении условия х > у, т.е. при х< у; б) после завершения цикла; в) в ходе выполнения цикла. Поскольку присваивание г:= х при х ~ 0 приводит к вхождению в цикл (так как из х ~ 0 следует х> О, г> 0), поэтому никаких других возможностей для г ~ О, кроме указанных трех, на структурной схеме не существует.
Рассмотрим последовательно эти три возможности: а) если х<у, то по структурной схеме г:= -1, т.е. г «О, а значит, х не делится на у в противоречие с допущением; б) если цикл завершен и г «О, то г < О. Это означает, что х — lсу < < О, т.е. х < Ау, и — (3 и я Щх = лу). Следовательно, х не делится на у, что также противоречит допущению; е) г ~ 0 в ходе выполнения цикла. Но в этом случае мы и не требуем, чтобы был дан ответ на вопрос о делимости х на у. Мы рассчитываем его получить после выполнения программы, а не в ходе ее выполнения. Но только что было доказано, что если цикл завершится с г ~ О, то х на у не делится. Здесь мы обнаруживаем, что цикл может и не завершиться, если г будет оставаться положительным.
Это будет происходить в том случае, когда у = 0 и г — 0 = г = х > О. Но так и должно быть: ведь в этом случае мы будем пьггаться установить, делится ли положительное число х на О, а такая операция запрещена. Таким образом, мы устанавливаем, что если наша программа завершится, то она решит поставленную задачу, т.е. мы доказали частичную правильность нашей программы. Чтобы сделать нашу программу тотально правильной, нужно предусмотреть ее завершение и в выявленном исключительном случае. Для этого можно, например, перед проверкой условия х > у проверить утверждение «х > 0 л у= 0». Если оно истинно, перейти к присваиванию г:= -1, если же оно ложно — перейти к проверке х > у. В заключение отметим, что исследования по логическому описанию программ и программирования убедительно показали, что логический анализ позволяет анализировать концепции языков программирования и находить многие скрытые недоработки в этих концепциях.
Пожалуй, до сих пор это применение строгих математических методов в качестве инструмента критики концепций (зачастую совершенно не продуманных, вставляемых ради «усиления» языков программирования) является важнейшим применением математической логики в области программирования. й 39. Применение компьютеров для доказательства теорем математической логики Мы уже отмечали, что формальные аксиоматические теории с их четкими понятиями аксиом и правил вывода, казалось бы, созданы для того, чтобы их развитие поручить электронно-вычислительной машине. И конечно же самым первым претенден- 397 том на союз с компьютером является формализованное исчисление высказываний.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
