Защищенный командный язык - Guarded Command Language

Guarded Command Language ( ГКЛ ) представляет собой язык определяется Эдсгер Дейкстры для предикатных трансформаторные семантики . Он компактно сочетает в себе концепции программирования, прежде чем программа будет написана на каком-либо практическом языке программирования. Его простота упрощает доказательство правильности программ с использованием логики Хоара .

Охраняемая команда

Защищенная команда - самый важный элемент защищенного командного языка. В охраняемой команде, как следует из названия, команда «охраняемая». Страж - это предложение , которое должно быть истинным до того, как оператор будет выполнен . В начале выполнения этого оператора можно предположить, что защита верна. Кроме того, если защита ложна, оператор не будет выполнен. Использование охранявших команд облегчает доказать программа соответствует спецификации . Заявление часто является еще одной охраняемой командой.

Синтаксис

Защищенная команда - это утверждение вида G → S, где

Если G истинно, охраняемая команда может быть записана просто S.

Семантика

В тот момент, когда G встречается в вычислении, он оценивается.

  • Если G истинно, выполнить S
  • Если G ложно, посмотрите на контекст, чтобы решить, что делать (в любом случае не выполняйте S)

Пропустить и отменить

Skip и Abort - это очень простые, а также важные операторы на защищенном командном языке. Abort - это неопределенная инструкция: делать что угодно. Оператор прерывания даже не требует завершения. Он используется для описания программы при формулировании доказательства, и в этом случае доказательство обычно терпит неудачу. Skip - это пустая инструкция: ничего не делать. Он используется в самой программе, когда синтаксис требует оператора, но программист не хочет, чтобы машина меняла состояния .

Синтаксис

skip

abort

Семантика

  • Пропустить: ничего не делать
  • Прервать: сделать что-нибудь

Назначение

Присваивает значения переменным .

Синтаксис

v := E

или 

v0, v1, ..., vn := E0, E1, ..., En

куда

  • v - программные переменные
  • E - выражения того же типа данных, что и соответствующие им переменные.

Конкатенация

Операторы разделяются точкой с запятой (;)

Выбор : если

Выбор (часто называемый «условным оператором» или «условным оператором») представляет собой список защищенных команд, из которых одна выбирается для выполнения. Если более чем одна защита верна, одно выражение недетерминированно выбирается для выполнения. Если ни один из охранников не соответствует действительности, результат не определен. Поскольку хотя бы один из охранников должен быть истинным, часто требуется пустое выражение «пропустить».

Синтаксис

if G0 → S0
| G1 → S1
...
| Gn → Sn
fi

Семантика

После выполнения отбора оцениваются все охранники. Если ни один из охранников не оценивается как истинный, то выполнение выбора прерывается, в противном случае одно из охранников, имеющее значение «истина», выбирается недетерминированно, и выполняется соответствующий оператор.

Примеры

Простой

В псевдокоде : 

if a < b then
  set c to True
else
  set c to False

На защищенном командном языке: 

if a < b → c := true
| a ≥ b → c := false
fi

Использование пропуска

В псевдокоде: 

if error is True then 
  set x to 0

На защищенном командном языке: 

if error = true → x := 0
| error = false → skip
fi

Если второй охранник опущен и error = False, результат отменяется.

Больше охранников правда

if a ≥ b → max := a
| b ≥ a → max := b
fi

Если a = b, либо a, либо b выбирается в качестве нового значения для максимума с одинаковыми результатами. Однако кто-то, реализующий это, может обнаружить, что один проще или быстрее другого. Поскольку для программиста нет никакой разницы, он может реализовать любой способ.

Повторение : делать

При повторении охраняемые команды выполняются повторно до тех пор, пока ни один из охранников не станет верным. Обычно охранник один.

Синтаксис

do G0 → S0
| G1 → S1
...
| Gn → Sn
od

Семантика

При выполнении повтора оцениваются все охранники. Если все охранники оценивают значение false, выполняется пропуск. В противном случае недетерминированно выбирается одна из защитных мер, имеющая значение true, и выполняется соответствующий оператор, после чего повторение выполняется снова.

Примеры

Оригинальный алгоритм Евклида

a, b := A, B;
do a < b → b := b - a
 | b < a → a := a - b
od

Это повторение заканчивается, когда a = b, и в этом случае a и b содержат наибольший общий делитель A и B.

Дейкстра видит в этом алгоритме способ синхронизации двух бесконечных циклов a := a - bи b := b - aтаким образом, что a≥0и b≥0остается верным.

Расширенный алгоритм Евклида

a, b, x, y, u, v := A, B, 1, 0, 0, 1;
do b ≠ 0 →
   q, r := a div b, a mod b;
   a, b, x, y, u, v := b, r, u, v, x - q*u, y - q*v
od

Это повторение заканчивается, когда b = 0, и в этом случае переменные содержат решение тождества Безу : xA + yB = gcd (A, B).

Недетерминированная сортировка

do a>b → a, b := b, a
 | b>c → b, c := c, b
 | c>d → c, d := d, c
od

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

Макс.

x, y = 1, 1 
do x≠n →
   if f(x) ≤ f(y) → x := x+1
    | f(x) ≥ f(y) → y := x; x := x+1
   fi
od

Этот алгоритм находит значение 1 ≤ y ≤ n, для которого заданная целочисленная функция f максимальна. Не только вычисления, но и конечное состояние не обязательно определяется однозначно.

Приложения

Программы правильные по построению

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

Асинхронные схемы

Защищенные команды подходят для проектирования схем с квази-нечувствительностью к задержкам, поскольку повторение допускает произвольные относительные задержки для выбора различных команд. В этом приложении логический вентиль, управляющий узлом y в схеме, состоит из двух охраняемых команд, а именно: 

PullDownGuard → y := 0
PullUpGuard → y := 1

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

Проверка модели

Защищенные команды используются в языке программирования Promela , который используется программой проверки модели SPIN . SPIN проверяет правильность работы параллельных программных приложений.

Другой

Модуль Perl Commands :: Guarded реализует детерминированный исправляющий вариант защищенных команд Дейкстры.

использованная литература

  1. ^ Дейкстра, Эдсгер Вт . «EWD472: Защищенные команды, неопределенность и формальное создание программ» (PDF) . Проверено 16 августа 2006 года .
  2. ^ Энн Kaldewaij (1990), Программирование: вывод алгоритмов , Prentice Hall
  3. Перейти ↑ Back, Ralph J (1978). «О правильности шагов уточнения при разработке программ (кандидатская диссертация)» (PDF) . Архивировано из оригинального (pdf) на 2011-07-20.
  4. ^ Мартин, Ален Дж. "Синтез асинхронных схем СБИС" .