Корректность (информатика)

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

В рамках этого понятия различают частичную корректность, требующую, чтобы если ответ возвращён, то он будет правильным, и полную корректность, которая дополнительно требует, чтобы ответ обязательно был возвращён, то есть алгоритм завершался. Соответственно, чтобы доказать полную корректность программы, достаточно доказать её частичную корректность и завершимость^[2]. Доказательство завершимости (доказательство завершения) не может быть полностью автоматизировано, поскольку проблема остановки является неразрешимой.

// возвращает сумму собственных делителей n
static int divisorSum(int n) {
   int i, sum = 0;
   for (i=1; i<n; ++i)
      if (n % i == 0)
         sum += i;
   return sum;
}
// возвращает наименьшее нечётное совершенное число
int leastPerfectNumber(void) {
   int n;
   for (n=1; ; n+=2)
      if (n == divisorSum(n))
         return n;
}

Например, последовательный перебор целых чисел 1, 2, 3, … с целью найти пример некоторого явления — например, нечётного совершенного числа — позволяет легко написать частично корректную программу (см. пример выше). Однако утверждать, что эта программа полностью корректна, означало бы утверждать нечто, что в настоящее время неизвестно в теории чисел.

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

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

Логика Хоара — это специальная формальная система для строгого рассуждения о корректности компьютерных программ^[3]. Она использует аксиоматические методы для определения семантики языков программирования и рассуждения о корректности программ с помощью утверждений, известных как тройки Хоара.

Тестирование программного обеспечения — это любая деятельность, направленная на оценку свойства или возможности программы или системы и определение того, что она соответствует требуемым результатам. Несмотря на важность для качества программного обеспечения и широкое применение программистами и тестировщиками, тестирование программ остаётся во многом искусством из-за ограниченного понимания принципов построения программ. Сложность тестирования обусловлена сложностью самих программ: невозможно полностью протестировать даже программу средней сложности. Тестирование — это не только отладка. Его цели могут включать обеспечение качества, верификацию и валидацию, а также оценку надёжности. Тестирование также может использоваться как универсальная метрика. Корректностное тестирование и тестирование надёжности — две основные области тестирования. Тестирование программного обеспечения — это компромисс между бюджетом, временем и качеством^[4].