Info21 писал(а):
Валерий Лаптев писал(а):
как это писать "под доказательство"?
Ой. Хороший вопрос, но полный ответ требует подготовки материала.
На самом грубом уровне разница видна здесь:
http://www.inr.ac.ru/~info21/texts/2005 ... ide13.htmlhttp://www.inr.ac.ru/~info21/texts/2005 ... ide14.htmlДве программы эквивалентны. Но правильность первой была установлена предварительным преобразованием ко второй.
Вторая -- как раз "под доказательство".
Да, хорошо видать разницу.
Однако меня и при первом прочтении книги Дейкстры, и сейчас не покидает мысль, что написание "под доказательство" касается только самого начального программирования.
То есть максимум до уровня написания процедур и функций.
В любой промышленной системе есть развитое окружение, которое частенько позволяет заменить показанные вами проги одной строкой.
Таким образом, получается, что Дейкстрины методы хороши при обучении программированию, при создании стандартных библиотек.
Ну, и если промышленному программеру действительно приходится писать нетривиальные процедуры. Однако если следовать советам экстремальных программистов, то размер методов следует ограничивать 1-5 строками. Тут и без всякого доказательства все сразу видать.
В промышленном программировании гораздо более важным является хорошая декомпозиция. Причем на всех уровнях (см. опять же Дейкстра - архитектура THE).
А в этом деле формальные методы фактически отсутствуют. И что с этим делать - пока неясно. Полно книжек с советами, как надо делать, или как делать не надо.
Однако все это - только опыт экспертов.