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

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

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

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

пока $x$ >0 делать $x$ := $x$ -1 из

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

если $x$ >0 тогда $x$ := $x$ –1; ( $x$ ≥0 ⇒ $x'$ =0) еще $ok$ быть ⇒ ( $x$ ≥0 ⇒ $x'$ =0)

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

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

если $x$ >0 тогда $x$ := $x$ –1; $t$ := $t$ +1; ( $x$ ≥0 ⇒ $t'$ = $t$ + $x$ ) ∧ ( $x$ <0 ⇒ $t'$ =∞) иначе $ok$ быть ⇒ ( $x$ ≥0 ⇒ $t'$ = $t$ + $x$ ) ∧ ( $x$ <0 ⇒ $t'$ =∞)

где $ok$ = ( $x'$ = $x$ ∧ $t'$ = $t$ ).

Библиография [ править ]

ECR Hehner, Практическая теория программирования , Springer-Verlag, 1993. Последнее онлайн-издание на сайте « Практическая теория программирования» .

Внешние ссылки [ править ]

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

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