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

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

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

Частично правильная программа на C, чтобы найти
наименьшее нечетное совершенное число,
его полная правильность неизвестна по состоянию на 2023 год.

// 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, …, чтобы увидеть, сможем ли мы найти пример какого-то явления — скажем, нечетного совершенного числа — довольно легко написать частично правильную программу (см. Вставку). Но сказать, что эта программа полностью правильна, значит утверждать что-то, что в настоящее время неизвестно в теории чисел .

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

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

Логика Хоара — это особая формальная система строгого рассуждения о правильности компьютерных программ. ^[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. Интернет.

[functional-1] Данлоп, Дуглас Д.; Базили, Виктор Р. (июнь 1982 г.). «Сравнительный анализ функциональной корректности» . Коммуникации АКМ . 14 (2): 229–244. дои : 10.1145/356876.356881 . S2CID 18627112 .

[totalcorrectness-2] Манна, Зоар; Пнуэли, Амир (сентябрь 1974 г.). «Аксиоматический подход к тотальной корректности программ». Акта Информатика . 3 (3): 243–263. дои : 10.1007/BF00288637 . S2CID 2988073 .

[hoare-3] Хоар, ЦАР (октябрь 1969 г.). «Аксиоматическая основа компьютерного программирования» (PDF) . Коммуникации АКМ . 12 (10): 576–580. CiteSeerX 10.1.1.116.2392 . дои : 10.1145/363235.363259 . S2CID 207726175 . Архивировано из оригинала (PDF) 4 марта 2016 года.

[4] Пан, Цзяньтао (весна 1999 г.). «Тестирование программного обеспечения» (курсовая работа). Университет Карнеги-Меллон . Проверено 21 ноября 2017 г.

[1]

[2]

[3]

[4]