Предикативное программирование - Predicative programming

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

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

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

пока ${ displaystyle x}$>0 делать ${ displaystyle x}$:= ${ displaystyle x}$–1 od

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

если ${ displaystyle x}$>0 тогда ${ displaystyle x}$:= ${ displaystyle x}$–1; (${ displaystyle x}$≥0 ⇒ ${ displaystyle x '}$=0) еще ${ displaystyle ok}$ фи ⇒ (${ displaystyle x}$≥0 ⇒ ${ displaystyle x '}$=0)

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

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

если ${ displaystyle x}$>0 тогда ${ displaystyle x}$:= ${ displaystyle x}$–1; ${ displaystyle t}$:= ${ displaystyle t}$+1; (${ displaystyle x}$≥0 ⇒ ${ displaystyle t '}$=${ displaystyle t}$+${ displaystyle x}$) ∧ (${ displaystyle x}$<0 ⇒ ${ displaystyle t '}$=∞) еще ${ displaystyle ok}$ фи ⇒ (${ displaystyle x}$≥0 ⇒ ${ displaystyle t '}$=${ displaystyle t}$+${ displaystyle x}$) ∧ (${ displaystyle x}$<0 ⇒ ${ displaystyle t '}$=∞)

куда ${ displaystyle ok}$ = (${ displaystyle x '}$=${ displaystyle x}$ ∧ ${ displaystyle t '}$=${ displaystyle t}$).

Библиография

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

внешняя ссылка

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

Этот формальные методы -связанная статья является заглушка. Вы можете помочь Википедии расширяя это.