Корректность (информатика)
В теоретической информатике алгоритм , является правильным по отношению к спецификации если он ведет себя так, как указано. Лучше всего исследовать функциональную корректность, которая относится к поведению алгоритма ввода-вывода (т. е. для каждого ввода он выдает результат, удовлетворяющий спецификации). [1]
В рамках последнего понятия частичная правильность , требующая, чтобы ответ был правильным, отличается от полной правильности , которая дополнительно требует, чтобы ответ в конечном итоге был возвращен, т. е. алгоритм завершается. Соответственно, чтобы доказать полную корректность программы, достаточно доказать ее частичную корректность и ее завершение. [2] Последний вид доказательства ( доказательство завершения может быть полностью автоматизирован, поскольку проблема остановки неразрешима ) никогда не .
| Частично правильная программа на C , чтобы найти наименьшее нечетное совершенное число, его полная правильность неизвестна по состоянию на 2023 год. |
// возвращаем сумму правильных делителей n
static int divisorSum ( int n ) {
int i , sum = 0 ;
for ( я знак равно 1 ; я < n ; ++ я )
если ( n % я == 0 )
сумма += я ;
возврата сумма ;
}
// возвращаем наименьшее нечетное совершенное число
int lessPerfectNumber ( void ) {
int n ;
for ( n = 1 ; ; n += 2 )
if ( n == divisorSum ( n ))
return n ;
}
|
Например, последовательно перебирая целые числа 1, 2, 3, …, чтобы увидеть, сможем ли мы найти пример какого-то явления — скажем, нечетного совершенного числа — довольно легко написать частично правильную программу (см. Вставку). Но сказать, что эта программа полностью правильна, значит утверждать нечто, чего в настоящее время не известно в теории чисел .
Доказательство должно быть математическим, при условии, что и алгоритм, и спецификация заданы формально. В частности, не ожидается, что это будет утверждением корректности данной программы, реализующей алгоритм на данной машине. Это потребует таких соображений, как ограничения на компьютерную память .
Глубокий результат в теории доказательств , соответствие Карри-Ховарда , утверждает, что доказательство функциональной корректности в конструктивной логике соответствует определенной программе в лямбда-исчислении . Преобразование доказательства таким способом называется извлечением программы .
Логика Хоара — это особая формальная система строгого рассуждения о правильности компьютерных программ. [3] Он использует аксиоматические методы для определения семантики языка программирования и доказательства правильности программ с помощью утверждений, известных как тройки Хоара.
Тестирование программного обеспечения — это любая деятельность, направленная на оценку атрибута или возможности программы или системы и определение того, соответствует ли она требуемым результатам. Хотя тестирование программного обеспечения имеет решающее значение для качества программного обеспечения и широко применяется программистами и тестировщиками, оно по-прежнему остается искусством из-за ограниченного понимания принципов программного обеспечения. Сложность тестирования программного обеспечения связана со сложностью программного обеспечения: мы не можем полностью протестировать программу средней сложности. Тестирование — это больше, чем просто отладка. Целью тестирования может быть обеспечение качества, проверка и валидация или оценка надежности. Тестирование также можно использовать в качестве общей метрики. Тестирование правильности и тестирование надежности — две основные области тестирования. Тестирование программного обеспечения — это компромисс между бюджетом, временем и качеством. [4]
См. также [ править ]
- Формальная проверка
- Проектирование по договору
- Анализ программы
- Проверка модели
- Корректность компилятора
- Вывод программы
Примечания [ править ]
- ^ Данлоп, Дуглас Д.; Базили, Виктор Р. (июнь 1982 г.). «Сравнительный анализ функциональной корректности» . Коммуникации АКМ . 14 (2): 229–244. дои : 10.1145/356876.356881 . S2CID 18627112 .
- ^ Манна, Зоар; Пнуэли, Амир (сентябрь 1974 г.). «Аксиоматический подход к тотальной корректности программ». Акта Информатика . 3 (3): 243–263. дои : 10.1007/BF00288637 . S2CID 2988073 .
- ^ Хоар, ЦАР (октябрь 1969 г.). «Аксиоматическая основа компьютерного программирования» (PDF) . Коммуникации АКМ . 12 (10): 576–580. CiteSeerX 10.1.1.116.2392 . дои : 10.1145/363235.363259 . S2CID 207726175 . Архивировано из оригинала (PDF) 4 марта 2016 года.
- ^ Пан, Цзяньтао (весна 1999 г.). «Тестирование программного обеспечения» (курсовая работа). Университет Карнеги Меллон . Проверено 21 ноября 2017 г.
Ссылки [ править ]
- « Технология человеческого языка. Проблемы информатики и лингвистики ». Гугл Книги. Нп и Интернет. 10 апреля 2017 г.
- « Безопасность в вычислительной технике и коммуникациях ». Гугл Книги. Нп и Интернет. 10 апреля 2017 г.
- « Проблема остановки Алана Тьюринга — самое веселое и иллюстрированное объяснение ». Проблема остановки Алана Тьюринга — самое веселое и иллюстрированное объяснение. Нп и Интернет. 10 апреля 2017 г.
- Тернер, Раймонд и Никола Ангиус. « Философия информатики ». Стэнфордская энциклопедия философии . Стэнфордский университет, 20 августа 2013 г. Интернет. 10 апреля 2017 г.
- Дейкстра, Э.В. «Корректность программы». Техасский университет в Остине, факультеты математики и компьютерных наук, проект автоматического доказательства теорем, 1970. Интернет.
