Статья 401

Программы пишутся с целью получить решения задач, а каждая правильно поставленная задача содержит в себе условие то, что дано и вопрос, на который нужно дать ответ. Если задача вообще поддается решению с помощью компьютера, ее условие превращается в предусловие, а вопрос преобразуется в постусловие, имеющее уже форму не вопроса, а утверждения, причем это утверждение должно быть истинно всякий раз, когда ответ на вопрос задачи правилен. Применительно к данным предусловию и постусловию пишется соответствующая программа, правильность которой необходимо доказать. Лучше всего делать это не после написания программы, а в ходе ее составления. Собственно, именно это и было проделано при решении задачи на делимость. Причем сначала была доказана частичная правильность программы, а затем, после небольшой модификации, и тотальная ее правильность по отношению к данной задаче. Доказательство убедило нас в том, что утверждение делится истинно при любых, удовлетворяющих предусловию если они вообще представимы на данном компьютере, но это обстоятельство подразумевается.