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

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

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

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

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

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

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

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

В Формализм Берд-Меертенса это подход к созданию программ.

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

Рекомендации

  • Эдсгер В. Дейкстра, Вим Х. Дж. Фейен, Метод программирования, Addison-Wesley, 1988, 188 стр.
  • Эдвард Коэн, Программирование в 1990-е годы, Springer-Verlag, 1990 г.
  • Энн Калдевай, Программирование: вывод алгоритмов, Прентис-Холл, 1990, 216 страниц.
  • Дэвид Грис, Наука программирования, Springer-Verlag, 1981, 350 стр.
  • Кэрролл Морган (ученый-компьютерщик), Программирование из спецификаций, Международная серия по информатике (2-е изд.), Прентис-Холл, 1998.
  • Эрик К.Р. Хенер, Практическая теория программирования, 2008, 235 стр.
  • А.Дж.М. ван Гастерен. О форме математических аргументов. Lecture Notes in Computer Science # 445, Springer-Verlag, 1990. Обучает четкому и точному написанию доказательств.
  • Мартин Рем. "Небольшие упражнения по программированию", появившиеся в Наука компьютерного программирования, Том 3 (1983) - Том 14 (1990).
  • Роланд Бэкхаус. Построение программы: расчет реализаций на основе спецификаций. Wiley, 2003. ISBN  978-0-470-84882-1.
  • Деррик Г. Кури, Брюс В. Уотсон. Подход к программированию, основанный на построении корректности. Springer-Verlag, 2012. ISBN  978-3-642-27919-5. Предоставляет пошаговое объяснение того, как выводить математически правильные алгоритмы с использованием небольших и удобных уточнений.