Вывод программы - 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 . Предоставляет пошаговое объяснение того, как выводить математически правильные алгоритмы с использованием небольших и удобных уточнений.