Прогнозирующее программирование
-
Основы предикативного программирования
- Предикативное программирование — метод спецификации и уточнения программ.
- Спецификация представляет собой двоичное выражение, истинное для приемлемого поведения и ложное для неприемлемого.
- Уточнение — это вывод из спецификации.
-
Применение и универсальность
- Метод применим к различным типам программ, включая последовательные, параллельные, автономные и взаимодействующие.
- Включает временные и пространственные границы.
-
Связь с командами в языке программирования
- Команды в языке программирования являются частным случаем спецификаций, которые могут быть скомпилированы.
-
Примеры спецификаций и их интерпретация
- Пример спецификации:
- x
- ′
- {\отображаемый стиль x’}
- =
- y
- {\displaystyle y}
- +1 ∧
- {\displaystyle y’}
- ∧
- z
- {\отображаемый стиль z’}
- {\displaystyle z}
- Пример уточнения:
- {\displaystyle x}
- :=
- +1 ⇒
- >
-
Определение времени выполнения
- Время выполнения можно определить, введя временную переменную.
- Доказательство завершения: доказать конечность времени выполнения.
- Доказательство бесконечности: доказать бесконечность времени выполнения.
-
Рекомендации и внешние ссылки
- Ссылки на публикации Эрика Хенера и предложение помощи Википедии в расширении статьи.