Статья 441

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

программа

программа


Итак, нет оснований считать теорему, полученную компьютером в ходе выполнения правильной программы, менее надежной, чем теорему, доказанную человеком. В принципиальном отношении между этими способами обоснования разницы нет. Тем самым мы еще раз убеждаемся в важности процедур и понятий, связанных с доказательствами правильности программ.

Доказательство правильности программ с помощью временной логики.

В этом параграфе мы обратимся к верификации компьютерных программ с помощью языковых и дедуктивных средств временной логики. За последнее десятилетие эта ветвь модальной логики получила применение как в области изучения искусственного интеллекта, так и в области разработки программного обеспечения.