Корректность программы

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

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

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

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

Теорема корректности. Программа P корректна относительно отношения спецификации r если и только если:

domain(r  P) = domain(r)

Доказательство:

Выражение r  P идентифицирует все приемлемые пары r, вычисляемые P. Следовательно, domain(r  P) идентифицирует множество входных данных, для которых P производит приемлемые выходные данные. Поскольку domain(r) – множество входных данных, для которых r определяет приемлемые выходные данные, условие

domain(r  P) = domain(r)

гарантирует, что P производит приемлемые выходные данные для каждого экземпляра входных данных, определяемых r. Что и требовалось доказать.

P может выполняться успешно для входных данных не заданных r, но такие пары P исключаются (r  P). Если P производит неприемлемые экземпляры выходных данных,

в (r  P) не существует элемента с соответствующими входными данными, и, следовательно, domain(r  P) не сможет быть равным domain(r).

Например, если:

r = {<A, †A†>, <B, †A†>, <A, †B†>, <B, †B†>}

и

P = {<x, x>: x - символ}

тогда

r  P = {<A, †A†>, <B, †B†>}

и

domain(r  P) = domain(r) = {A, B}

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

Следствие. Программа P корректна относительно функции спецификации f если и только если:

f  P

Основной вопрос программирования

Основной вопрос программирования и точно, основной вопрос программиста, пытающегося соответствовать спецификации, может быть сформулирован просто:

Для данных спецификации и программы, соответствует ли программа спецификации?

Неформально, если ответ на этот вопрос – «да», то говорят, что программа корректна в соответствии со спецификацией. Более формально, для данного отношения спецификации программы r и программы P, мы говорим, что программа P корректна относительно r, если для каждого элемента x области определения r (экземпляра входных данных), P производит элемент области значений r, который соответствует x. То есть, для каждого входного x, P производит y, такой что <x, y>  r.

Что выполняет P для входных данных, не принадлежащих области определения r несущественно, поскольку r определяет все поведение важное в контексте решения задачи. Это определение сводится к чисто теоретико-множественной идее, сформулированной в следующей теореме:

Теорема корректности. Программа P корректна относительно отношения спецификации r если и только если:

domain(r  P) = domain(r)

Доказательство:

Выражение r  P идентифицирует все приемлемые пары r, вычисляемые P. Следовательно, domain(r  P) идентифицирует множество входных данных, для которых P производит приемлемые выходные данные. Поскольку domain(r) – множество входных данных, для которых r определяет приемлемые выходные данные, условие

domain(r  P) = domain(r)

гарантирует, что P производит приемлемые выходные данные для каждого экземпляра входных данных, определяемых r. Что и требовалось доказать.

P может выполняться успешно для входных данных не заданных r, но такие пары P исключаются (r  P). Если P производит неприемлемые экземпляры выходных данных,

в (r  P) не существует элемента с соответствующими входными данными, и, следовательно, domain(r  P) не сможет быть равным domain(r).

Например, если:

r = {<A, †A†>, <B, †A†>, <A, †B†>, <B, †B†>}

и

P = {<x, x>: x - символ}

тогда

r  P = {<A, †A†>, <B, †B†>}

и

domain(r  P) = domain(r) = {A, B}

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

Следствие. Программа P корректна относительно функции спецификации f если и только если:

f  P