Читать онлайн «Доказательство правильности программ»

PROVING PROGRAMS CORRECT ROBERT В ANDERSON University of Houston . ;j John Wiley & Sons New York Chichester Brisbane Toronto 1979 Р Андерсон ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ ПРОГРАММ Перевод с английского Б. Н. 30БНИН0Й лод редакцией д-ра фйз. -мат. наук Д. Б. ПОДПШВАЛОВА Москва «Мир» 1982 ' ББК 32. 973 А65 УДК 6813. 06 Андерсон Р. А65 Доказательство правильности программ: Пер. с англ. — М. : Мир, 1982. -168 с, ил. В книге американского специалиста изложены основные принципы доказательства правильности программ для ЭВМ. Принципы доказательства иллюстрируются многочисленными примерами программ, представленных блок-схемами или записанных на языках высокого уровня. Материал излагается в простой и доступной форме. Для пользователей ЭВМ, аспирантов и студентов, изучающих программирование. л 30502-126 ■126-82, 4. 1 2405000000 ББК 32. 973 041(01>-82 Редакция литературы по новой технике Copyright © 1979 by John Wiley & Sons, Inc. All rights reserved. Authorized translation from English language edition published by John Wiley & Sons, Inc. © Перевод на русский язык, «Мир», 1982 ПРЕДИСЛОВИЕ РЕДАКТОРА ПЕРЕВОДА Почти 15 лет назад было высказано предположение, что правильность программ для ЭВМ можно доказывать так же, как, например, доказываются теоремы в математике. Любой программист либо специалист, использующий ЭВМ в своей практике, отчетливо представляет себе актуальность этой проблемы. С одной стороны, машины стали не только использоваться в научных расчетах, где можно контролировать решение на основе некоторых качественных представлений о его характере, но и включаться в автоматизировайные или полностью автоматические системы управления, в которых человек не может контролировать процессы или из-за временных ограничений, или просто потому, что от него ускользает именно качественная картина процессов. С другой стороны, дискретная природа современных систем обработки информации не позволяет говорить о «в принципе верной» или «качественно верной» программе: любая самая незначительная ошибка может приводить к самым фантастическим результатам именно в силу этой дискретности. Таким образом, проблема доказательства правильности программ и еще более общая проблема создания надежных программ оказались выдвинутыми на первый план именно благодаря практическим соображениям. Книга, которую читатель держит в руках, — первая книга на русском языке, в которой довольно объективно обсуждается проблема доказательства правильности программ. От читателя не требуется каких-либо специальных математических знаний для ее понимания. В ней объясняется постановка задачи: что такое «правильность программы» и как можно доказать эту правильность? Книга в основном построена на примерах — фактически это только примеры с небольшими вкраплениями «теории» и рассуждений общего характера. б Предисловие редактора перевода Автор как опытный педагог не пытается навязать вам заранее свое мнение. Примеры говорят сами за себя. Хотя эта книга и не о программировании, она предназначена для программистов.