Прогнозирующее программирование

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

Команды на языке программирования считаются особым случаем спецификации - те спецификации, которые можно компилировать. Например, если программными переменными являются $x\; \{\backslash \; displaystyle\; x\}$, $y\; \{\backslash \; displaystyle\; y\}$и $z\; \{\backslash \; displaystyle\; z\}$, команда $x\; \{\backslash \; displaystyle\; x\}$: = $y\; \{\backslash \; displaystyle\; y\}$+1 эквивалентна спецификации (двоичное выражение) $x\; \prime \; \{\backslash \; displaystyle\; x\; \text{'}\}$=$y\; \{\backslash \; displaystyle\; y\}$+1 ∧ $y\; \prime \; \{\backslash \; displaystyle\; y\text{'}\}$=$y\; \{\backslash \; displaystyle\; y\}$∧ $z\; \prime \; \{\; \backslash \; displaystyle\; z\; \text{'}\}$=$z\; \{\backslash \; displaystyle\; z\}$, в котором $x\; \{\backslash \; displaystyle\; x\}$, $y\; \{\backslash \; displaystyle\; y\}$и $z\; \{\backslash \; displaystyle\; z\}$представляют значения программных переменных до назначения, а $x\; \prime \; \{\backslash \; displaystyle\; x\; \text{'}\}$, $y\; \prime \; \{\backslash \; displaystyle\; y\text{'}\}$и $z\; \prime \; \{\backslash \; displaystyle\; z\; \text{'}\}$представляют значения переменных программы после присвоения. Если спецификация имеет вид $x\; \prime \; \{\backslash \; displaystyle\; x\; \text{'}\}$>$y\; \{\backslash \; displaystyle\; y\}$, мы легко докажем ($x\; \{\backslash \; displaystyle\; x\}$: = $y\; \{\backslash \; displaystyle\; y\}$+1) ⇒ ($x\; \prime \; \{\backslash \; displaystyle\; x\; \text{'}\}$>$y\; \{\backslash \; displaystyle\; y\}$), в котором говорится, что $x\; \{\backslash \; displaystyle\; x\}$: = $y\; \{\backslash \; displaystyle\; y\}$+1 подразумевает, уточняет или реализует $x\; \prime \; \{\; \backslash \; displaystyle\; x\; \text{'}\}$>$y\; \{\backslash \; displaystyle\; y\}$.

Циклическое доказательство значительно упрощено. Например, если $x\; \{\backslash \; displaystyle\; x\}$является целочисленной переменной, чтобы доказать, что

while$x\; \{\backslash \; displaystyle\; x\}$>0 do$x\; \{\backslash \; displaystyle\; x\}$: = $x\; \{\backslash \; displaystyle\; x\}$–1 od

уточняет или реализует спецификацию $x\; \{\backslash \; displaystyle\; x\}$≥0 ⇒ $x\; \prime \; \{\backslash \; displaystyle\; x\; \text{'}\}$= 0, доказать

if$x\; \{\backslash \; displaystyle\; x\}$>0, затем$x\; \{\backslash \; displaystyle\; x\}$: = $x\; \{\backslash \; displaystyle\; x\}$–1; ($x\; \{\backslash \; displaystyle\; x\}$≥0 ⇒ $x\; \prime \; \{\backslash \; displaystyle\; x\; \text{'}\}$= 0) else$хорошо\; \{\backslash \; displaystyle\; ok\}$fi⇒ ($x\; \{\backslash \; displaystyle\; x\}$≥0 ⇒ $x\; \prime \; \{\backslash \; displaystyle\; x\; \text{'}\}$= 0)

где $хорошо\; \{\backslash \; displaystyle\; ok\}$= ($x\; \prime \; \{\backslash \; displaystyle\; x\; \text{'}\}$=$x\; \{\backslash \; displaystyle\; x\}$) равно пустая команда или команда ничего не делать. Нет необходимости в инварианте цикла или с наименьшей фиксированной точкой. Петли с несколькими промежуточными неглубокими и глубокими выходами работают одинаково. Эта упрощенная форма доказательства возможна, потому что программные команды и спецификации могут быть осмысленно смешаны вместе.

Время выполнения (верхняя граница, нижняя граница, точное время) можно доказать таким же образом, просто введя временную переменную. Чтобы доказать прекращение, докажите, что время выполнения конечно. Чтобы доказать отсутствие прекращения действия, докажите, что время выполнения бесконечно. Например, если переменная времени $t\; \{\backslash \; displaystyle\; t\}$, а время измеряется путем подсчета итераций, то для доказательства того, что выполнение предыдущего while -loop требует время $x\; \{\backslash \; displaystyle\; x\}$, когда $x\; \{\backslash \; displaystyle\; x\}$изначально неотрицательно, и продолжается вечно, когда $x\; \{\backslash \; displaystyle\; x\}$изначально отрицательно, докажите

if$x\; \{\backslash \; displaystyle\; x\}$>0, затем$x\; \{\backslash \; displaystyle\; x\}$: = $x\; \{\backslash \; displaystyle\; x\}$–1; $т\; \{\backslash \; displaystyle\; t\}$: = $t\; \{\backslash \; displaystyle\; t\}$+1; ($икс\; \{\backslash \; displaystyle\; x\}$≥0 ⇒ $t\; \prime \; \{\backslash \; displaystyle\; t\; \text{'}\}$=$t\; \{\backslash \; displaystyle\; t\}$+$x\; \{\backslash \; displaystyle\; x\}$) ∧ ($Икс\; \{\backslash \; Displaystyle\; x\}$<0 ⇒ $t\; \prime \; \{\backslash \; Displaystyle\; t\; \text{'}\}$= ∞) else$хорошо\; \{\backslash \; Displaystyle\; ок\}$fi⇒ ($х\; \{\backslash \; displaystyle\; x\}$≥0 ⇒ $t\; \prime \; \{\backslash \; displaystyle\; t\; \text{'}\}$=$t\; \{\backslash \; displaystyle\; t\}$+$x\; \{\; \backslash \; displaystyle\; x\}$) ∧ ($x\; \{\backslash \; displaystyle\; x\}$<0 ⇒ $t\; \prime \; \{\backslash \; displaystyle\; t\; \text{'}\}$= ∞)

где $хорошо\; \{\backslash \; displaystyle\; ok\}$= ($x\; \prime \; \{\backslash \; displaystyle\; x\; \text{'}\}$=$x\; \{\backslash \; displaystyle\; x\}$∧ $t\; \prime \; \{\backslash \; displaystyle\; t\text{'}\}$=$т\; \{\backslash \; displaystyle\; t\}$).

• E.C.R. Хенер, Практическая теория программирования, Springer-Verlag, 1993. Последнее онлайн-издание на Практическая теория программирования.

• Публикации Эрика Хенера.

.