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

На практике доказывать программы оказывается довольно непривычно. Для этого нужно понять, что мы хотим доказать. Формулировка: Мы хотим доказать, что программа работает правильно, является крайне расплывчатой. Не помогает заменить правильность на отсутствие ошибок, так как это, очевидно, тавтология.

Чтобы что-то доказать, мы должны сформулировать теоремы, которые собственно и будем доказывать.

Я встречался в статьях со следующими формулировками:

  • Доказать, что цикл завершается у Дейкстры
  • Доказательство, что определенная формула верна, например частное умножить на делитель плюс остаток равно исходному числу у Хоара
  • Доказательство свойства взаимного исключения, отсутствия дедлоков и живучести алгоритмов синхронизации у Лампорта

Таким образом, когда у нас есть определенная программа мы должны определить интересные нам свойства и доказать, что они выполняются. В этом плане довольно просто доказывать функции без побочных эффектов. Нам надо чтобы за конечное число шагов такая функция получила результат, а значит надо доказать:

  • Асимптотику выполнения программы, за О каких шагов выполнится алгоритм
  • Доказать, что выходные значения будут удовлетворять некоторой формуле, входит в какие-то множества и так далее

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