WikiDer > Защищенный командный язык

Эта статья нужны дополнительные цитаты для проверка. Пожалуйста помоги улучшить эту статью к добавление цитат в надежные источники. Материал, не полученный от источника, может быть оспорен и удален. Найдите источники: «Защищенный командный язык» – Новости · газеты · книги · ученый · JSTOR (Декабрь 2010 г.) (Узнайте, как и когда удалить этот шаблон сообщения)

В Защищенный командный язык (GCL) - это язык, определяемый Эдсгер Дейкстра за семантика преобразователя предикатов.^[1] Он компактно сочетает в себе концепции программирования, прежде чем программа будет написана на каком-либо практическом языке программирования. Его простота упрощает проверку правильности программ с помощью Логика Хоара.

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

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

Синтаксис

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

• G - это предложение, позвал охранника
• S - это заявление

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

Семантика

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

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

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

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

Синтаксис

пропускать

прервать

Семантика

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

Назначение

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

Синтаксис

v: = E

или же

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

куда

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

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

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

Выбор: если

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

Синтаксис

если G0 → S0 | G1 → S1 ... | Gn → Snфи

Семантика

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

Примеры

Простой

В псевдокод:

если a

иначе c: = Ложь

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

если a фи

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

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

если error = True, то x: = 0

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

если error = true → x: = 0 | ошибка = ложь → пропускатьфи

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

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

если a ≥ b → max: = a | b ≥ a → max: = bфи

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

Репетиция: делать

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

Синтаксис

делать G0 → S0 | G1 → S1 ... | Gn → Snod

Семантика

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

Примеры

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

а, b: = А, В;делать a od

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

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

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

a, b, x, y, u, v: = A, B, 1, 0, 0, 1;делать b ≠ 0 → | q, r: = a div б, а мод б; | a, b, x, y, u, v: = b, r, u, v, x - q * u, y - q * vod

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

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

делать a> b → a, b: = b, a | b> c → b, c: = c, b | c> d → c, d: = d, cod

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

Макс

х, у = 1, 1 делать x ≠ n → | если f (x) ≤ f (y) → x: = x + 1 | | f (x) ≥ f (y) → y: = x; х: = х + 1 | фиod

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

Приложения

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

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

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

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

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

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

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

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

Другой

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

Рекомендации