Спецификация, моделирование и программирование принципиально одинаковы, верно?

Question

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

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

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

Итак, можем ли мы делать все эти вещи одновременно, потому что они принципиально одинаковы? Является ли декларативное программирование ближайшей попыткой сделать это? Можем ли мы использовать какие-то языки программирования, которые будут хороши для программирования, а также для моделирования и спецификации?

Answer 1

Ученый, который сделал больше всего для продвижения этой точки зрения, - Тони Хоар. Тони вместе со своим коллегой Эдсгером Дейкстрой отстаивали недетерминированные языки программирования, чтобы был более плавный путь от спецификации к реализации. Тони определенно хотел один язык как для спецификации, так и для реализации. Подробнее об этом представлении читайте в его книге по Alegbra of Programming . Тони также сделал основную работу по доказательству правильности абстракций. Вся эта работа была проделана в контексте простых императивных языков со структурированным потоком управления и классическими процедурами с побочными эффектами. Так что нет никакой связи с декларативным программированием необходимости. Исторически сложилось так, что работа над функциональным программированием (основной ветвью декларативного программирования) стала продолжением лекции Тьюринга Бэкуса об «освобождении программирования от узкого места фон Неймана»; Функциональное программирование было связано с производительностью программирования так же, как и с чем угодно.

То, что мы обнаружили со времен Хоара, заключается в том, что формальные спецификации и формальные модели * очень дорогие . Расходы не были оправданы, за исключением особых обстоятельств, таких как «если программное обеспечение не работает, пациент умрет» или «если программное обеспечение не будет работать, самолет упадет». Неформальные модели и спецификации довольно полезны, и их гораздо дешевле производить и работать. По-прежнему проводятся интересные исследования в области моделирования, проверки моделей и так далее. Один из моих любимых - это язык Alloy, созданный группой Дэниела Джексона в MIT. В Microsoft Research также есть отличная работа и много других хороших вещей. Также есть некоторая работа в декларативном программировании, но она также имеет «дешевое и веселое» разнообразие, а не всеобъемлющий, программный подход, как у Хоара. Один из моих любимых - это QuickCheck от Claessen и Hughes, который предоставляет возможность устанавливать формальные свойства и исследовать их путем случайного тестирования. Никаких доказательств или теорем, но все же очень полезно.

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