Вывод программы - Program derivation

В информатике , программа вывод является выводом программы из его спецификации, математическими средствами.

Чтобы получить программу , средства , чтобы написать формальную спецификацию, которая, как правило , не исполняемым, а затем применить математически правильные правила для того , чтобы получить исполняемую программу , удовлетворяющую эту спецификацию. Полученная таким образом программа является правильной по построению. Программа и доказательство корректности строятся вместе.

Подход, обычно применяемый при формальной проверке, заключается в том, чтобы сначала написать программу, а затем предоставить доказательство того, что она соответствует заданной спецификации . Основные проблемы с этим заключаются в том, что

  • получаемое доказательство часто бывает длинным и громоздким;
  • нет информации о том, как была разработана программа; выглядит «как кролик из шляпы»;
  • если программа окажется некорректной в какой-то неуловимой форме, попытка проверить ее, вероятно, будет долгой и наверняка будет бесплодной.

Разработка программы пытается исправить эти недостатки с помощью

  • сокращение доказательств за счет разработки соответствующих математических обозначений;
  • принятие проектных решений путем формального изменения спецификации.

Термины, которые примерно синонимичны термину «создание программ»: трансформационное программирование, алгоритмика, дедуктивное программирование.

Птица-Meertens формализм является подход к программе вывода.

Смотрите также

Ссылки

  • Эдсгер В. Дейкстра , Вим Х. Дж. Фейен, Метод программирования , Аддисон-Уэсли, 1988, 188 страниц
  • Эдвард Коэн, Программирование в 1990-х , Springer-Verlag, 1990
  • Энн Калдевай, Программирование: вывод алгоритмов , Прентис-Холл, 1990, 216 страниц.
  • Дэвид Грис, Наука программирования , Springer-Verlag, 1981, 350 страниц.
  • Кэрролл Морган (специалист по информатике) , Программирование на основе спецификаций , International Series in Computer Science (2-е изд.), Prentice-Hall, 1998.
  • Эрик CR Hehner , Практическая теория программирования , 2008, 235 страниц
  • AJM van Gasteren. О форме математических аргументов . Конспект лекций по информатике № 445, Springer-Verlag, 1990. Обучает четкому и точному написанию доказательств.
  • Мартин Рем. «Небольшие упражнения по программированию», появившиеся в Science of Computer Programming , Vol.3 (1983) - Vol.14 (1990).
  • Роланд Бэкхаус. Построение программы: расчет реализаций по спецификациям . Wiley, 2003. ISBN  978-0-470-84882-1 .
  • Деррик Г. Кури, Брюс В. Уотсон. Подход к программированию, основанный на построении корректности . Springer-Verlag, 2012. ISBN  978-3-642-27919-5 . Предоставляет пошаговое объяснение того, как выводить математически правильные алгоритмы с использованием небольших и удобных уточнений.