Я знаю несколько способов убедиться в корректности программы:

  • Провести тестирование
  • Провести мысленный эксперимент с целью понять как программа работает
  • Строго доказать корректность программы, на основе теорем выведенных из аксиом

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

Почему мне хочется строго доказывать корректность программы? Этому есть простое объяснение. Тестирование и мысленные эксперименты не работают. Мысленный эксперимент в моем случае не работает совсем и подводит в 90% случаев. На практике получается, что пока не запустишь программу, сказать будет ли она работать или нет - нельзя.

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

Так как два способа написания программ без ошибок в моем случае не работают, я хочу попробовать третий. В надежде, что он станет серебряной пулей. Что, конечно, не так, не станет. Самый базовый способ доказательства корректности это использование статически типизированных языков. Я использую Java и Typescript, еще Dart, но с ним как-то у меня плохие отношения, не нравится совсем. Типизация спасает от дурацких ошибок и помогает при рефакторинге, но работает при правильном проектировании программы. Если вы повсюду используете ассоциативные массивы, в виде HashMap или чего-то подобного, никакая типизация вас не спасет. Опять же в Java типизация не спасает от самой распространенной ошибки NullPointerException.

Можно не ограничиваться доказательством соответствия типов переменных, а пойти дальше и следуя Флойду, Лампорту и Хоару доказывать корректность программ строго математически. И на самом деле, это обязательно делать в случае многопоточных программ. В программах, выполняемых в нескольких потоках вообще очень плохо работает мысленный эксперимент и еще хуже работают тесты. Проблема с доказательством в том, что формальные доказательства очень длинные и не владея методом практически невозможно прийти к методике. Надо знать требования к строгости доказательства и уметь строить доказательства, а этому в большинстве вузов не учат. Во всяком случае, средний студент по моему опыту этим не владеет. В строго доказанной программе могут быть ошибки, но они довольно быстро находятся. Я верю Дейкстре, который смог полностью доказать даже такую большую программу, как операционная система. Дейкстра утверждал, что в его ОС, ошибки были либо простыми опечатками, либо очень быстро фиксились из-за того, что явно противоречили ходу доказательства.