Защищенный командный язык
Язык защищенных команд ( GCL ) — это язык программирования, определенный Эдсгером Дейкстрой для семантики преобразователя предикатов в EWD472. [1] Он компактно сочетает в себе концепции программирования. Это упрощает разработку программы и ее доказательства рука об руку, при этом идеи доказательства лидируют; более того, части программы действительно могут быть рассчитаны .
Важным свойством GCL является недетерминированность . Например, в операторе if несколько альтернатив могут быть истинными, и выбор того, какой из них выбрать, делается во время выполнения, когда выполняется оператор if. Это освобождает программиста от необходимости делать ненужный выбор и помогает формально разрабатывать программы.
GCL включает оператор множественного присваивания. Например, выполнение оператора x, y:= y, x выполняется путем сначала оценки значений правой части, а затем сохранения их в левых переменных. Таким образом, этот оператор меняет местами значения х и и .
В следующих книгах обсуждается разработка программ с использованием GCL :
- Дейкстра, Эдсгер В. (1976). Дисциплина программирования . Прентис Холл. ISBN 978-0132158718 .
- Грис, Д. (1981). Наука программирования . Монографии по информатике (на английском, испанском, японском, китайском, итальянском и русском языках). Нью-Йорк: Springer Verlag. дои : 10.1007/978-1-4612-5983-1 . ISBN 978-0-387-96480-5 . S2CID 37034126 .
- Дейкстра, Эдсгер В .; Фейен, Вим Х.Дж. (1988). Метод программирования . Бостон, Массачусетс: Addison-Wesley Longman Publishing Co., Inc. п. 200. ИСБН 978-0-201-17536-3 .
- Калдевайдж, Энн (1990). Программирование: вывод алгоритмов . Прентис-Холл, Inc. ISBN 0132041081 .
- Коэн, Эдвард (1990). Дэвид Грайс (ред.). Программирование в 1990-е годы: Введение в расчет программ . Тексты и монографии по информатике. Спрингер Верлаг. дои : 10.1007/978-1-4613-9706-9 . ISBN 978-1-4613-9706-9 . S2CID 1509875 .
Охраняемая команда
[ редактировать ]Защищенная команда состоит из логического условия или Guard и оператора, «защищенного» им. Оператор выполняется только в том случае, если защита истинна, поэтому при рассуждении об операторе условие можно считать истинным. Это облегчает подтверждение того, что программа соответствует спецификации .
Защищенная команда — это оператор вида G → S, где
- G — это предложение , называемое охраной
- S – это утверждение
- Если G оценивается как истина, S может быть выполнен. В большинстве конструкций GCL несколько защищенных команд могут иметь истинные ограничения, и ровно одна из них произвольно выбирается для выполнения.
- Если G ложно, S не будет выполнено.
пропустить и прервать
[ редактировать ]Пропустить и прервать — важные операторы защищенного командного языка. abort — это неопределенная инструкция: делайте что угодно. Даже прекращать работу не нужно. Он используется для описания программы при формулировании доказательства, и в этом случае доказательство обычно терпит неудачу. Пропустить — пустая инструкция: ничего не делать. Он часто используется, когда синтаксис требует оператора, но состояние не должно меняться.
Синтаксис
[ редактировать ]skip
abort
Семантика
[ редактировать ]- пропустить : ничего не делать
- прервать : сделать что-нибудь
Присваивает значения переменным .
Синтаксис
[ редактировать ]v := E
или
v0, v1, ..., vn := E0, E1, ..., En
где
- v are program variables
- E — выражения того же типа данных , что и соответствующие им переменные.
катенация
[ редактировать ]Операторы разделяются одной точкой с запятой (;)
Выбор : если
[ редактировать ]Выбор (часто называемый «условным оператором» или «оператором if») представляет собой список защищенных команд, из которых одна выбирается для выполнения. Если более одной защиты истинна, для выполнения произвольно выбирается один оператор, защита которого истинна. Если ни одно предупреждение не истинно, результат не определен, то есть эквивалентен прерыванию . Поскольку хотя бы один из охранников должен быть истинным, пропуск часто требуется пустого оператора. В утверждении if fi нет защищенных команд, поэтому настоящей защиты никогда не бывает. Следовательно, если fi эквивалентно abort .
Синтаксис
[ редактировать ]if G0 → S0 □ G1 → S1... □ Gn → Snfi
Семантика
[ редактировать ]При выполнении выбора охранники оцениваются. Если ни один из охранников не является истинным , то выбор прерывается, в противном случае одно из предложений с истинным охранником выбирается произвольно, и его оператор выполняется.
Выполнение
[ редактировать ]GCL не определяет реализацию. Поскольку защитные меры не могут иметь побочных эффектов , а выбор предложения произволен, реализация может оценивать защитные меры в любой последовательности и выбирать первое истинное , например, предложение.
Примеры
[ редактировать ]Простой
[ редактировать ]В псевдокоде :
if a < b then set c to Trueelse set c to False
На защищенном командном языке:
if a < b → c := true □ a ≥ b → c := falsefi
Использование пропуска
[ редактировать ]В псевдокоде:
if error is True then set x to 0
На защищенном командном языке:
if error → x := 0 □ error → skipfi
Если второй предохранитель опущен и ошибка имеет значение False, результат прерывается.
Больше охранников правда
[ редактировать ]if a ≥ b → max := a □ b ≥ a → max := bfi
Если a = b, либо a, либо b выбирается в качестве нового значения максимума с одинаковыми результатами. Однако реализация может обнаружить, что один из них проще или быстрее другого. Поскольку для программиста нет никакой разницы, подойдет любая реализация.
Повторение : сделать
[ редактировать ]Выполнение этого повторения или цикла показано ниже.
Синтаксис
[ редактировать ]do G0 → S0 □ G1 → S1... □ Gn → Snod
Семантика
[ редактировать ]Выполнение повторения состоит из выполнения 0 или более итераций , причем итерация состоит из произвольного выбора защищенной команды Gi → Si , защита Gi которой истинна, и выполнения команды Si . Таким образом, если все охранники изначально ложны, повторение немедленно прекращается, без выполнения итерации. При выполнении повторения do od , у которого нет защищенных команд, выполняется 0 итераций, поэтому do od эквивалентен Skip .
Примеры
[ редактировать ]Оригинальный алгоритм Евклида
[ редактировать ]a, b := A, B;do a < b → b := b - a □ b < a → a := a - bod
Это повторение заканчивается, когда 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*vod
Это повторение заканчивается, когда 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, cod
Программа продолжает переставлять элементы, пока один из них больше, чем его преемник. Эта недетерминированная пузырьковая сортировка не более эффективна, чем ее детерминированная версия, но ее легче доказать: она не остановится, пока элементы не отсортированы, и на каждом этапе сортируется как минимум 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 fiod
Этот алгоритм находит значение 1 ≤ y ≤ n , для которого заданная целочисленная функция f является максимальной. Не только вычисление, но и конечное состояние не обязательно определяется однозначно.
Приложения
[ редактировать ]Программы правильные по построению
[ редактировать ]Обобщение наблюдательного соответствия охраняемых команд в решетку привело к усовершенствованному исчислению . [2] Это было механизировано в формальных методах, таких как B-метод , которые позволяют формально выводить программы из их спецификаций.
Асинхронные схемы
[ редактировать ]Защищенные команды подходят для проектирования схем, квазинечувствительных к задержке, поскольку повторениедопускает произвольные относительные задержки для выбора различных команд. В этом приложениилогический элемент, управляющий узлом y в схеме, состоит из двух защищенных команд, а именно:
PullDownGuard → y := 0PullUpGuard → y := 1
PullDownGuard и PullUpGuard здесь являются функциями входов логического элемента,которые описывают, когда ворота понижают или повышают выходной сигнал соответственно. В отличие от классическогоВ моделях оценки схемы повторение набора защищенных команд (соответствующих асинхронной схеме) может точно описать все возможные динамические поведения этой схемы.В зависимости от модели, с которой можно жить для элементов электрической схемы,для описания защищенной команды могут потребоваться дополнительные ограничения на защищенные команды.быть полностью удовлетворительным. Общие ограничения включают стабильность, невмешательство и отсутствиесамоопровергающихся команд. [3]
Проверка модели
[ редактировать ]Защищенные команды используются в языке программирования Promela , который используется средством проверки моделей SPIN . SPIN проверяет правильность работы параллельных программных приложений.
Другой
[ редактировать ]Модуль Perl Commands::Guarded реализует детерминированный, исправляющий вариант защищенных команд Дейкстры.
Ссылки
[ редактировать ]- ^ Дейкстра, Эдсгер В. «EWD472: Защищенные команды, неопределенность и формальный вывод программ» (PDF) . Проверено 16 августа 2006 г.
- ^ Назад, Ральф Дж (1978). «О правильности этапов усовершенствования при разработке программы (кандидатская диссертация)» (PDF) . Архивировано из оригинала (PDF) 20 июля 2011 г.
- ^ Мартин, Ален Дж. «Синтез асинхронных схем СБИС» .
