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