Верификация программы: фундаментальные проблемы информатики

Одной из наиболее важных проблем, стоящих перед информатикой, является разработка парадигмы, соответствующей этой дисциплине. Сторонники формальных методов, такие как Джон Маккарти, C.A.R. Хоар и Эдгар Дейкстра выдвинули точку зрения, что вычислительная техника — это математическая деятельность и что информатика должна моделировать себя по образцу математики. Противники формальных методов, напротив, предполагают, что программирование является фундаментальной деятельностью в информатике и что существуют важные различия, отличающие его от математики, которая, следовательно, не может обеспечить подходящую парадигму. Разногласия по поводу места формальных методов в информатике недавно возникли в форме возобновления интереса к природе и возможностям верификации программ как метода установления надежности программных систем. Статья Джеймса Х. Фетцера под названием «Программная верификация: сама идея», появившаяся в «Communications of the ACM», вызвала обширную дискуссию, которая обсуждалась в нескольких журналах и продолжалась в течение нескольких лет, привлекая интерес ученых-компьютерщиков (как теоретических, так и прикладных), а также других мыслителей самого широкого круга, которые хотят понять информатику как область исследований. Редакторы этого сборника собрали множество наиболее интересных и важных исследований, которые помогают ответить на вопросы о природе и пределах информатики. К ним относятся ранние статьи, защищающие математическую парадигму Маккарти, Наура, Р. Флойда и Хоара (в части I), другие, которые разработали парадигму Хоара, Мейера, Наура, Шерлиса и Скотта (в части II), проблемы, ограничения и альтернативы, исследованные К. Флойдом, Смитом, Блюмом и Науром (в части III), а также недавние работы, посвященные формальной проверке ДеМилло, Липтона и Перлис, Фетцер, Кон и Колберн (в части IV). Он предоставляет необходимые ресурсы для дальнейшего изучения. Этот том понравится учёным, философам [...]