Одним из важных методов повышения эффективности проектирования программ является верификация программ или математическое доказательство того, что программа работает правильно. Для доказательства правильности программ используется аксиоматический подход, при котором применяется теория перечисления предикатов. Предполагается, что каждый оператор в программе выполняет заранее определенные действия, зависящие только от синтаксиса языка. Для двух предикатов P и Q и оператора S необходимо определить, истинно ли выражение:
«Если P истинно и если выполняется оператор S, то Q истинно».
Предикат P является спецификацией правильного выполнения оператора S, а предикат Q будет истинным после выполнения оператора S и является спецификацией следующего за S оператора.
Если это утверждение распространить на все операторы программы и если P является спецификацией первого оператора, а Q истинно после окончания программы, то будет доказана правильность всей программы относительно предикатов P и Q. Эту конструкцию можно записать в следующем виде:
где P называется предусловием истинности Q после выполнения программы S.
Доказательство правильности программы заключается в определении, является ли выражение {P}S{Q} истинным относительно входных спецификаций P, выходных спецификаций Q и операторов S программы. Если {P}S{Q} истинно, то это означает, что доказана правильность программы S относительно P и Q.