Корректность (информатика) - Correctness (computer science)

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

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

Частично правильная программа на C для поиска
наименьшего нечетного совершенного числа,
ее полная корректность неизвестна по состоянию на 2021 год.
// return the sum of proper divisors of n
static int divisorSum(int n) {
   int i, sum = 0;
   for (i=1; i<n; ++i)
      if (n % i == 0)
         sum += i;
   return sum;
}
// return the least odd perfect number
int leastPerfectNumber(void) {
   int n;
   for (n=1; ; n+=2)
      if (n == divisorSum(n))
         return n;
}

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

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

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

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

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

Смотрите также

Примечания

использованная литература