> -- Info21 писал(а):
> Ой. Хороший вопрос, но полный ответ требует подготовки материала. На самом грубом уровне разница видна здесь:Две программы эквивалентны. Но правильность первой была установлена предварительным преобразованием ко второй. Вторая -- как раз "под доказательство".
Да, хорошо видать разницу.
Однако меня и при первом прочтении книги Дейкстры, и сейчас не покидает мысль, что написание "под доказательство" касается только самого начального программирования.
То есть максимум до уровня написания процедур и функций.
В любой промышленной системе есть развитое окружение, которое частенько позволяет заменить показанные вами проги одной строкой.
Таким образом, получается, что Дейкстрины методы хороши при обучении программированию, при создании стандартных библиотек.
Ну, и если промышленному программеру действительно приходится писать нетривиальные процедуры. Однако если следовать советам экстремальных программистов, то размер методов следует ограничивать 1-5 строками. Тут и без всякого доказательства все сразу видать.

В промышленном программировании гораздо более важным является хорошая декомпозиция. Причем на всех уровнях (см. опять же Дейкстра - архитектура THE).
А в этом деле формальные методы фактически отсутствуют. И что с этим делать - пока неясно. Полно книжек с советами, как надо делать, или как делать не надо.
Однако все это - только опыт экспертов.