Jazyk hlídaného příkazu - Guarded Command Language

Hlídané Command Language ( GCL ) je jazyk, definovaný Edsger Dijkstra pro predikátu sémantiky transformátoru . Kombinuje programovací koncepce kompaktním způsobem, než je program napsán v nějakém praktickém programovacím jazyce. Jeho jednoduchost usnadňuje dokazování správnosti programů pomocí logiky Hoare .

Strážené velení

Strážený příkaz je nejdůležitějším jazykem hlídaného příkazu. V hlídaném příkazu, jak název napovídá, je příkaz „střežený“. Strážný je problém , který musí být splněny dříve, než je příkaz proveden . Na začátku provedení tohoto prohlášení lze předpokládat, že strážný je pravdivý. Pokud je strážný falešný, prohlášení nebude provedeno. Použití hlídaných příkazů usnadňuje prokázání, že program splňuje specifikaci . Prohlášení je často dalším střeženým příkazem.

Syntax

Střežený příkaz je příkaz ve tvaru G → S, kde

  • G je návrh , nazývaný strážný
  • S je prohlášení

Pokud je G pravdivé, lze hlídaný příkaz napsat jednoduše S.

Sémantika

V okamžiku, kdy se ve výpočtu objeví G, je vyhodnoceno.

  • Pokud je G pravda, spusťte S
  • Pokud je G nepravdivé, podívejte se na kontext a rozhodněte se, co dělat (v žádném případě neprovádějte S)

Přeskočit a přerušit

Skip and Abort jsou velmi jednoduchá a důležitá prohlášení v hlídaném příkazovém jazyce. Přerušení je nedefinovaný pokyn: dělat cokoli. Potvrzení o přerušení nemusí být ani ukončeno. Slouží k popisu programu při formulování důkazu, v takovém případě důkaz obvykle selže. Přeskočit je prázdný pokyn: nedělat nic. Používá se v samotném programu, kdy syntaxe vyžaduje příkaz, ale programátor nechce, aby stroj měnil stavy .

Syntax

skip

abort

Sémantika

  • Přeskočit: nedělat nic
  • Přerušit: udělat cokoli

Úkol

Přiřadí hodnoty proměnným .

Syntax

v := E

nebo 

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

kde

  • v jsou programové proměnné
  • E jsou výrazy stejného datového typu jako jejich odpovídající proměnné

Zřetězení

Příkazy jsou odděleny středníkem (;)

Výběr : pokud

Výběr (často nazývaný „podmíněný příkaz“ nebo „příkaz if“) je seznam hlídaných příkazů, z nichž je vybrán k provedení. Pokud je pravdivých více než jeden strážný, jedno prohlášení je nedeterministicky vybráno k provedení. Pokud žádný ze strážců není pravdivý, výsledek není definován. Protože alespoň jeden ze strážců musí být pravdivý, je často potřeba prázdné prohlášení „přeskočit“.

Syntax

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

Sémantika

Po provedení výběru jsou vyhodnoceni všichni strážci. Pokud žádný ze strážců nevyhodnotí hodnotu true, provedení výběru se přeruší, jinak je jeden ze strážců, který má hodnotu true, vybrán nedeterministicky a je provedeno odpovídající prohlášení.

Příklady

Jednoduchý

V pseudokódu : 

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

V hlídaném příkazovém jazyce: 

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

Použití přeskočení

V pseudokódu: 

if error is True then 
  set x to 0

V hlídaném příkazovém jazyce: 

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

Pokud je druhý strážný vynechán a chyba = False, výsledek se přeruší.

Více strážců pravda

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

Pokud a = b, je jako nová hodnota maxima zvoleno buď a nebo b, se stejnými výsledky. Někdo, kdo to implementuje , však může zjistit, že jeden je jednodušší nebo rychlejší než druhý. Vzhledem k tomu, že pro programátora není žádný rozdíl, může implementovat libovolným způsobem.

Opakování : do

Opakování provádí střežené příkazy opakovaně, dokud není žádný ze strážných pravdivý. Obvykle je tam jen jeden strážný.

Syntax

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

Sémantika

Po provedení opakování jsou vyhodnoceni všichni strážci. Pokud všichni strážci vyhodnotí jako nepravdivé, provede se přeskočení. Jinak je jeden ze strážců, který má hodnotu true, vybrán nedeterministicky a je provedeno odpovídající prohlášení, po kterém je opakování provedeno znovu.

Příklady

Originální euklidovský algoritmus

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

Toto opakování končí, když a = b, v takovém případě a a b mají největšího společného dělitele A a B.

Dijkstra vidí v tomto algoritmu způsob synchronizace dva nekonečné cykly a := a - ba b := b - atakovým způsobem, aby a≥0i b≥0nadále platí.

Rozšířený euklidovský algoritmus

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

Toto opakování končí, když b = 0, v takovém případě proměnné obsahují řešení Bézoutovy identity : xA + yB = gcd (A, B).

Nedeterministické řazení

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

Program pokračuje v permutaci prvků, zatímco jeden z nich je větší než jeho nástupce. Toto nedeterministické třídění bublin není účinnější než jeho deterministická verze, ale je snazší ho dokázat: nezastaví se, když prvky nejsou seřazeny a že v každém kroku seřadí alespoň 2 prvky.

Arg max

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

Tento algoritmus najde hodnotu 1 ≤ y ≤ n, pro kterou je daná celočíselná funkce f maximální. Nejen výpočet, ale také konečný stav není nutně jednoznačně určen.

Aplikace

Programy správné konstrukcí

Zobecnění pozorovací shody střežených příkazů na mříž vedlo k upřesnění kalkulu . Toto bylo mechanizováno ve formálních metodách, jako je B-metoda, které umožňují formálně odvodit programy z jejich specifikací.

Asynchronní obvody

Strážené příkazy jsou vhodné pro návrh obvodu necitlivého na kvazi zpoždění, protože opakování umožňuje libovolné relativní zpoždění pro výběr různých příkazů. V této aplikaci se logická brána pohánějící uzel y v obvodu skládá ze dvou hlídaných příkazů, a to následovně: 

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

PullDownGuard a PullUpGuard zde jsou funkce vstupů logické brány, které popisují, kdy brána táhne výstup dolů, respektive nahoru. Na rozdíl od klasických modelů vyhodnocení obvodu může opakování pro sadu hlídaných příkazů (odpovídajících asynchronnímu obvodu) přesně popsat všechna možná dynamická chování tohoto obvodu. V závislosti na modelu, s nímž jsme ochotni žít pro prvky elektrického obvodu, mohou být nutná další omezení hlídaných příkazů, aby byl popis hlídaného příkazu zcela uspokojivý. Mezi běžná omezení patří stabilita, nerušení a absence samočinných příkazů.

Kontrola modelu

Hlídané příkazy se používají v programovacím jazyce Promela , který používá kontrola modelu SPIN . SPIN ověřuje správnou činnost souběžných softwarových aplikací.

jiný

Modul Perl Commands :: Guarded implementuje deterministickou, napravující variantu na hlídané příkazy Dijkstra.

Reference

  1. ^ Dijkstra, Edsger W . „EWD472: Střežené příkazy, nerozhodnost a formální odvozování programů“ (PDF) . Citováno 16. srpna 2006 .
  2. ^ Anne Kaldewaij (1990), Programming: The Derivation of Algorithms , Prentice Hall
  3. ^ Zpět, Ralph J (1978). „O správnosti kroků upřesnění při vývoji programu (disertační práce)“ (PDF) . Archivováno z originálu (pdf) dne 2011-07-20.
  4. ^ Martin, Alain J. „Syntéza asynchronních obvodů VLSI“ .