GCL: язык программирования от Дейкстры для разработки и доказательства программ. Компактный синтаксис, недетерминизм и возможность вычисления частей кода.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Язык программирования с защищёнными командами (GCL) — это язык программирования, определённый Эдсгером Дейкстрой для семантики преобразования предикатов в EWD472. Он объединяет концепции программирования в компактной форме. Это облегчает одновременную разработку программы и её доказательства, при этом идеи доказательства задают направление; более того, части программы могут быть фактически вычислены. Важным свойством GCL является недетерминированность. Например, в операторе if несколько альтернатив могут быть истинными, и выбор, какую из них выбрать, осуществляется во время выполнения, когда оператор if выполняется. Это освобождает программиста от необходимости делать ненужные выборы и помогает в формальной разработке программ. GCL включает оператор множественного присваивания. Например, выполнение оператора осуществляется путём сначала вычисления значений правой части, а затем сохранения их в левые переменные. Таким образом, этот оператор меняет местами значения и . Следующие книги посвящены разработке программ с использованием GCL:
The Guarded Command Language (GCL) is a programming language defined by Edsger Dijkstra for predicate transformer semantics in EWD472. It combines programming concepts in a compact way. It makes it easier to develop a program and its proof hand in hand, with the proof ideas leading the way; moreover, parts of a program can actually be calculated. An important property of GCL is nondeterminism. For example, in the if statement, several alternatives may be true, and the choice of which to choose is done at runtime, when the if statement is executed. This frees the programmer from having to make unnecessary choices and is an aid in the formal development of programs. GCL includes the multiple assignment statement. For example, execution of the statement is done by first evaluating the righthand side values and then storing them in the lefthand variables. Thus, this statement swaps the values of and
The following books discuss the development of programs using GCL:
Охраняемая команда
Защищенная команда является наиболее важным элементом языка защищенных команд. В защищенной команде, как следует из названия, команда "охраняется" условием. Это условие – логическое выражение, которое должно быть истинным перед выполнением команды. В начале выполнения команды можно считать, что условие истинно. Кроме того, если условие ложно, команда выполняться не будет. Использование защищенных команд упрощает доказательство соответствия программы спецификации. Команда часто сама является защищенной командой.
The guarded command is the most important element of the guarded command language. In a guarded command, just as the name says, the command is "guarded". The guard is a proposition, which must be true before the statement is executed. At the start of that statement's execution, one may assume the guard to be true. Also, if the guard is false, the statement will not be executed. The use of guarded commands makes it easier to prove the program meets the specification. The statement is often another guarded command.
Пропусти и отмени
skip и abort – важные операторы в языке защищённых команд. abort – это неопределённая инструкция: делайте всё, что угодно. Ему даже не обязательно завершать работу. Он используется для описания программы при построении доказательства, в этом случае доказательство обычно не удаётся. skip – пустая инструкция: ничего не делать. Он используется в самой программе, когда синтаксис требует оператора, но состояние не должно изменяться.
skip and abort are important statements in the guarded command language. abort is the undefined instruction: do anything. It does not even need to terminate. It is used to describe the program when formulating a proof, in which case the proof usually fails. skip is the empty instruction: do nothing. It is used in the program itself, when the syntax requires a statement but the state should not change.
Назначение
Присваивает значения переменным.
Assigns values to variables.
Выбор: если
Выбор (часто называемый "условным оператором" или "оператором if") представляет собой список команд с условиями, из которых одна выбирается для выполнения. Если более одного условия истинно, то недетерминированно выбирается для исполнения одна из команд, условие которой истинно. Если ни одно условие не истинно, результат не определен. Поскольку по крайней мере одно условие должно быть истинным, часто требуется пустая команда skip. Оператор if fi не содержит команд с условиями, поэтому ни одно условие никогда не будет истинным. Следовательно, if fi эквивалентен прерыванию.
The selection (often called the "conditional statement" or "if statement") is a list of guarded commands, of which one is chosen to execute. If more than one guard is true, one statement whose guard is true is nondeterministically chosen to be executed. If no guard is true, the result is undefined. Because at least one of the guards must be true, the empty statement skip is often needed. The statement if fi has no guarded commands, so there is never a true guard. Hence, if fi is equivalent to abort.
Семантика
После выполнения выбора оцениваются все условия. Если ни одно из условий не возвращает true, выполнение выбора прерывается, иначе одно из условий, возвращающих значение true, выбирается недетерминированно, и выполняется соответствующее выражение.
Upon execution of a selection all guards are evaluated. If none of the guards evaluates to true then execution of the selection aborts, otherwise one of the guards that has the value true is chosen non deterministically and the corresponding statement is executed.
Повторение:
Исполнение этого повтора, или цикла, показано ниже.
Execution of this repetition, or loop, is shown below.
Семантика
Исполнение повторения состоит из выполнения 0 или более итераций, где итерация состоит из (недетерминированного) выбора охраняемой команды Gi → Si, у которой охрана Gi истинна, и выполнения команды Si. Таким образом, если все стражи изначально ложны, повторение завершается немедленно, без выполнения какой-либо итерации. Исполнение повторения do od, которое не содержит охраняемых команд, выполняет 0 итераций, следовательно, do od эквивалентно команде skip.
Execution of the repetition consists of executing 0 or more iterations, where an iteration consists of (nondeterministically) choosing a guarded command Gi → Si whose guard Gi evaluates to true and executing the command Si. Thus, if all guards are initially false, the repetition terminates immediately, without executing an iteration. Execution of the repetition do od, which has no guarded commands, executes 0 iterations, so do od is equivalent to skip.
Программы корректны по конструкции
Обобщение наблюдательной конгруэнтности охраняемых команд в решетку положило начало речевому исчислению (Refinement Calculus). Это было реализовано в формальных методах, таких как метод B, позволяющий формально выводить программы из их спецификаций.
Generalizing the observational congruence of Guarded Commands into a lattice has led to Refinement Calculus. This has been mechanized in Formal Methods like B Method that allow one to formally derive programs from their specifications.
Проверка модели
Защищённые команды используются в языке программирования Promela, который применяется в системе проверки моделей SPIN. SPIN верифицирует корректность работы параллельных программных приложений.
Guarded commands are used within the Promela programming language, which is used by the SPIN model checker. SPIN verifies correct operation of concurrent software applications.
Другое
Модуль Perl Commands::Guarded реализует детерминированный, самовосстанавливающийся вариант защищенных команд Дейкстры.
The Perl module Commands::Guarded implements a deterministic, rectifying variant on Dijkstra's guarded commands.