В теоретической информатике алгоритм является правильным относительно спецификации , если он ведет себя так, как указано. Лучше всего изучена функциональная корректность, которая относится к поведению алгоритма на входе-выходе: для каждого входа он производит выход, удовлетворяющий спецификации. [1]
В рамках последнего понятия частичная корректность , требующая, чтобы ответ, если он будет возвращен, был правильным, отличается от полной корректности , которая дополнительно требует, чтобы ответ был в конечном итоге возвращен, т. е. алгоритм завершается. Соответственно, чтобы доказать полную корректность программы, достаточно доказать ее частичную корректность и ее завершение. [2] Последний вид доказательства ( доказательство завершения ) никогда не может быть полностью автоматизирован, поскольку проблема остановки неразрешима .
Например, последовательно просматривая целые числа 1, 2, 3, …, чтобы увидеть, можем ли мы найти пример некоторого явления — скажем, нечетное совершенное число — довольно легко написать частично правильную программу (см. вставку). Но сказать, что эта программа полностью правильна, означало бы утверждать что-то, что в настоящее время неизвестно в теории чисел .
Доказательство должно быть математическим, предполагая, что и алгоритм, и спецификация даны формально. В частности, не ожидается, что это будет утверждением корректности для данной программы, реализующей алгоритм на данной машине. Это повлечет за собой такие соображения, как ограничения на память компьютера .
Глубокий результат в теории доказательств , соответствие Карри–Ховарда , утверждает, что доказательство функциональной корректности в конструктивной логике соответствует определенной программе в лямбда-исчислении . Преобразование доказательства таким образом называется извлечением программы .
Логика Хоара — это особая формальная система для строгого рассуждения о корректности компьютерных программ. [3] Она использует аксиоматические методы для определения семантики языка программирования и аргументации о корректности программ с помощью утверждений, известных как тройки Хоара.
Тестирование программного обеспечения — это любая деятельность, направленная на оценку атрибута или возможности программы или системы и определение того, что она соответствует требуемым результатам. Несмотря на то, что оно имеет решающее значение для качества программного обеспечения и широко применяется программистами и тестировщиками, тестирование программного обеспечения по-прежнему остается искусством из-за ограниченного понимания принципов программного обеспечения. Трудность тестирования программного обеспечения проистекает из сложности программного обеспечения: мы не можем полностью протестировать программу с умеренной сложностью. Тестирование — это больше, чем просто отладка. Целью тестирования может быть обеспечение качества, верификация и валидация или оценка надежности. Тестирование также может использоваться в качестве общей метрики. Тестирование корректности и тестирование надежности — это две основные области тестирования. Тестирование программного обеспечения — это компромисс между бюджетом, временем и качеством. [4]