Есть три аксиомы Шура-Бура:
1) В каждой программе есть хотя бы одна ошбка.
2) Если в ней нет ошибки, то неверен алгоритм.
3) Если нет ошибки и алгорифм верен, то программа никому не нужна.
В трудах отцов-основателей сермяжная (она же посконная) правда часто проступает. Поражает глубина их понимания проблематики.
Чуть-чуть более серьезно:
Debiloid писал(а):
Не абстракция. Есть методы, однако.
Доказательство правильности программы, коли память ветренная мне не изменяет с другими, суть проблема алгоритмически неразрешимая (аки следствие немца Гёделя теоремы).
bekas писал(а):
Это следует из простого подсчета всевозможных логических путей прохождения алгоритма, [...] И тут не помогут никакие методы a-la автоматического доказательства правильности программ. Мы можем только надеяться, что наша программа будет работать только в ОПРЕДЕЛЕННЫХ УСЛОВИЯХ.
Вы не вполне корректны. Программы, правильность которых серьезно интересует, не тестируют, а доказывают. Математическое же доказательство позволяет высказываться о произвольных объектах, что ему комбинаторный взрыв, не более чем счетный по природе своей.
К сожалению, во многих современных курсах программирования большое внимание уделяется объектно-ориентированному анализу и объектно-ориентированному проектированию. Многие как-бы не замечают, что объектно-ориентированного программирования нет, есть лишь структурное. И все изучение структурного сводят к знаменитой цитате "goto считать вредным". Между тем, Дейкстра и другие (я вспомню Хоара (Взаимодействие последовательных процессов), на меня лично сильно повлиял Грис (Наука программирования) -
книга Дейкстры не была доступна) определяли структурное программирование иначе - как
доказательное программирование, id est процесс, при котором правильность программы доказывют. Процесс сей не может быть полностью автоматизирован, как и доказательство математической теоремы, и я верю
Debiloid - он может быть автоматизирован частично.
Главным же его недостатком является стоимость (zum Beispiel, я потратил вечер - около 6 часов - для доказательства правильности 15 строк программы. Мне было очень нужно
). Он очень утомителен и очень дорог. В результате используется практиками (даже владеющими методом, хотя таких и меньшинство) весьма редко, только при написании весьма ответственного кода. Пример
Майера меня мало впечатлил. Интересно, что американский стандарт на критические приложения DO-178 вооще не допускает "мертвого" кода (хотя тут еще надо разобратьься, что такое мертвый код). Всяк со своим опытом может сравнить. Но то, что дорого - определенно. А качество суть категория экономическая. Посему почти всяк начальник любого программиста, пишущего математически безошибочные программы уволит, как медленно работающего. (почти все - по определению - кроме множества меры ноль).
Посему программисты выбирают не доказывать.
Я беседывал однажды с одним начальником "от программирования". Беседа шла почти дружески, и я позволил себе высказаться в том смысле, что security программы вообще нельзя отлаживать. Он страшно обиделся: "Как это?!? Мы же отлаживаем!" Ну что можно сказать такому человеку? Пожалеть разве что. Его, и его клиентуру. А заодно и калечимых им его программистов.