Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

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

Различают частичную правильность , которая требует, чтобы если ответ был возвращен, он был правильным, и полной правильностью , которая дополнительно требует завершения работы алгоритма. Поскольку не существует общего решения проблемы остановки , полная правильность не разрешима . Терминации доказательство представляет собой тип математического доказательства , что играет важную роль в формальной верификации , так как общая корректность алгоритма зависит от завершения. [2]

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

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

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

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

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

См. Также [ править ]

Заметки [ править ]

  1. ^ Данлоп, Дуглас Д .; Базили, Виктор Р. (июнь 1982 г.). «Сравнительный анализ функциональной корректности» . Коммуникации ACM . 14 (2): 229–244. DOI : 10.1145 / 356876.356881 . CS1 maint: обескураженный параметр ( ссылка )
  2. ^ Манна, Зоар; Пнуэли, Амир (сентябрь 1974 г.). «Аксиоматический подход к абсолютной корректности программ». Acta Informatica . 3 (3): 243–263. DOI : 10.1007 / BF00288637 .
  3. Перейти ↑ Hoare, CAR (октябрь 1969). «Аксиоматическая основа компьютерного программирования» (PDF) . Коммуникации ACM . 12 (10): 576–580. CiteSeerX 10.1.1.116.2392 . DOI : 10.1145 / 363235.363259 . Архивировано из оригинального (PDF) 4 марта 2016 года.   CS1 maint: обескураженный параметр ( ссылка )
  4. ^ Pan, Jiantao (весна 1999). «Тестирование программного обеспечения» (курсовая). Университет Карнеги-Меллона . Проверено 21 ноября 2017 года .

Ссылки [ править ]

  • « Технология человеческого языка. Проблемы информатики и лингвистики ». Google Книги. Np, nd Web. 10 апреля 2017.
  • « Безопасность вычислений и коммуникаций ». Google Книги. Np, nd Web. 10 апреля 2017.
  • « Проблема остановки Алана Тьюринга - самое веселое и яркое объяснение ». Проблема остановки Алана Тьюринга - самое веселое и наглядное объяснение. Np, nd Web. 10 апреля 2017.
  • Тернер, Раймонд и Никола Ангиус. « Философия информатики ». Стэнфордская энциклопедия философии . Стэнфордский университет, 20 августа 2013 г. Web. 10 апреля 2017.
  • Дейкстра, Э.В. "Правильность программы". Университет Техаса в Остине, Отделение математики и компьютерных наук, Проект автоматического доказательства теорем, 1970. Web.