О противоречии между правильностью доказательств и правильностью реализации
В предыдущем разделе подразумевалась "точная арифметика"; мой опыт показывает, что обоснованность таких доказательств часто ставится под сомнение людьми, которые ссылаются на то, что на практике в нашем распоряжении никогда не бывает абсолютно точной арифметики: обычно имеется верхняя граница для допустимых целых значений; действительные числа представляются только с конечной точностью и т. д. Так в чем же ценность таких доказательств?
Мне кажется, что ответ на этот вопрос состоит в следующем. Если человек доказывает правильность программы применительно к идеализированному совершенному миру, то ему не следует удивляться, если что-то идет не так, когда эта идеальная программа выполняется на "несовершенной" машине. Это очевидно. Поэтому если мы хотим доказать правильность программы для более реального мира, то прежде всего необходимо четко осознать, что все используемые в программе операции (и, в частности, все арифметические операции) не обязательно выполняются точно; при этом мы должны сформулировать подобные аксиомам свойства, которым эти операции должны удовлетворять для того, чтобы программа выполнялась правильно, т. е. те свойства, на которых основывается доказательство правильности. (Для примера из предыдущего раздела требуется всего лишь точная целая арифметика в интервале [0,2a].)
При написании программы, работающей с действительными числами с приближенным выполнением операций, человек должен быть уверен, что выполняются некоторые предположения, такие, как b>0 означает, что
a*b=b*a
-(a*b)=(-a)*b
0*x=0
1*x=x и т. д.
Очень часто справедливость таких отношений оказывается существенной для логики программы. Чтобы обеспечить вычислимость, программисту следует быть как можно менее требовательным, но хорошая реализация должна удовлетворять как можно большему числу разумных требований.
Здесь уместно покаяться в одной моей ошибке. При реализации языка АЛГОЛ-60 мы решили, что отношение х=у будет принимать значение true не только в случае точного равенства, но также и тогда, когда значения х и у отличаются только в самом младшем разряде машинного представления, поскольку в противном случае было бы слишком маловероятно, что когда-нибудь удастся вычислить значение true.
Мы думали тогда о сходимости итераций, которые могли бы колебаться при ограниченной точности вычислений. Поскольку мы были очень щедры (с лучшими намерениями!) в трактовке действительных чисел как равных, часто выбранная нами операция сравнения оказывалась настолько слабой, что ее вообще вряд ли можно было использовать. Ситуация сводилась к тому, что программист, установив истинность отношений а=b и b=с, не имел права сделать вывод, что а=с. Мы быстро отказались от такого решения. На основании накопленного мною опыта такого рода я могу утверждать, что программист может использовать предоставленное ему средство программирования только с учетом определенных свойств этого средства; и наоборот, программист должен уметь сформулировать, какие именно свойства ему требуются. (Обычно программисты так не поступают, поскольку отсутствуют традиции отбора свойств, не требующих обоснования, и поэтому потребовалось бы утомительное перечисление слишком многих подробностей. Обильное распространение вычислительных машин с отвратительной аппаратной реализацией плавающей запятой, а также превратное представление, будто вычислительные машины предназначены непосредственно для специалистов по численному анализу, - все это нанесло большой ущерб программированию как профессии.)
