Strzeżony język poleceń — Guarded Command Language

Strzeżone Command Language ( GCL ) to język zdefiniowany przez Edsger Dijkstra dla bazowych semantyki transformatorowych . Łączy koncepcje programowania w zwarty sposób, zanim program zostanie napisany w jakimś praktycznym języku programowania. Jego prostota ułatwia udowodnienie poprawności programów za pomocą logiki Hoare'a .

Strzeżone polecenie

Strzeżone dowództwo jest najważniejszym elementem strzeżonego języka dowodzenia. W strzeżonym poleceniu, tak jak sama nazwa wskazuje, polecenie jest „strzeżone”. Strażnik to propozycja , która musi być prawdą przed oświadczenie jest wykonywane . Na początku egzekucji tego stwierdzenia można przyjąć, że strażnik jest prawdziwy. Ponadto, jeśli strażnik jest fałszywy, oświadczenie nie zostanie wykonane. Użycie strzeżonych poleceń ułatwia udowodnienie, że program spełnia specyfikację . Stwierdzenie to często jest kolejnym strzeżonym poleceniem.

Składnia

Polecenie strzeżone to stwierdzenie postaci G → S, gdzie

  • G to propozycja , zwana strażnikiem
  • S to stwierdzenie

Jeśli G jest prawdziwe, strzeżone polecenie można zapisać po prostu S.

Semantyka

W momencie napotkania G w obliczeniach jest ono oceniane.

  • Jeśli G jest prawdziwe, wykonaj S
  • Jeśli G jest fałszywe, spójrz na kontekst, aby zdecydować, co zrobić (w żadnym wypadku nie wykonuj S)

Pomiń i przerwij

Pomiń i przerwij to bardzo proste, a także ważne wyrażenia w strzeżonym języku poleceń. Abort jest niezdefiniowaną instrukcją: rób wszystko. Oświadczenie o przerwaniu nawet nie musi się kończyć. Służy do opisu programu podczas formułowania dowodu, w którym to przypadku dowód zwykle zawodzi. Pomiń to pusta instrukcja: nic nie rób. Jest używany w samym programie, gdy składnia wymaga instrukcji, ale programista nie chce, aby maszyna zmieniała stany .

Składnia

skip

abort

Semantyka

  • Pomiń: nic nie rób
  • Przerwij: rób cokolwiek

Zadanie

Przypisuje wartości do zmiennych .

Składnia

v := E

lub 

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

gdzie

  • v są zmiennymi programu
  • E to wyrażenia tego samego typu danych, co odpowiadające im zmienne

Powiązanie

Instrukcje są oddzielone jednym średnikiem (;)

Wybór : jeśli

Wybór (często nazywany „instrukcją warunkową” lub „instrukcją if”) jest listą strzeżonych poleceń, z których jedno jest wybrane do wykonania. Jeśli więcej niż jeden strażnik jest prawdziwy, jedna instrukcja jest wybierana do wykonania w sposób niedeterministyczny. Jeśli żaden ze strażników nie jest prawdziwy, wynik jest niezdefiniowany. Ponieważ przynajmniej jeden ze strażników musi być prawdziwy, często potrzebne jest puste stwierdzenie „pomiń”.

Składnia

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

Semantyka

Po dokonaniu selekcji oceniani są wszyscy strażnicy. Jeśli żaden ze strażników nie ma wartości prawda, to wykonanie selekcji zostanie przerwane, w przeciwnym razie jeden ze strażników, który ma wartość prawda, zostanie wybrany niedeterministycznie i zostanie wykonana odpowiednia instrukcja.

Przykłady

Prosty

W pseudokodzie : 

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

W strzeżonym języku poleceń: 

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

Korzystanie z pominięcia

W pseudokodzie: 

if error is True then 
  set x to 0

W strzeżonym języku poleceń: 

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

Jeśli drugi strażnik zostanie pominięty i błąd = False, wynik zostanie przerwany.

Więcej strażników prawdziwych

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

Jeśli a = b, jako nową wartość maksimum wybiera się a lub b, z równymi wynikami. Jednak ktoś, kto to zaimplementuje , może uznać, że jedno jest łatwiejsze lub szybsze od drugiego. Ponieważ nie ma różnicy dla programisty, może on zaimplementować w dowolny sposób.

Powtórzenie : do

Powtórzenie powoduje wykonanie strzeżonych poleceń wielokrotnie, aż żaden ze strażników nie jest prawdziwy. Zwykle jest tylko jeden strażnik.

Składnia

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

Semantyka

Po wykonaniu powtórki wszyscy strażnicy są oceniani. Jeśli wszystkie osłony mają wartość false, wykonywane jest pominięcie. W przeciwnym razie jeden ze strażników, który ma wartość true, zostanie wybrany niedeterministycznie i zostanie wykonana odpowiednia instrukcja, po czym powtórzenie zostanie wykonane ponownie.

Przykłady

Oryginalny algorytm Euklidesa

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

To powtórzenie kończy się, gdy a = b, w którym to przypadku aib mają największy wspólny dzielnik A i B.

Dijkstra widzi w tym algorytmie sposób na zsynchronizowanie dwóch nieskończonych cykli a := a - bi to b := b - aw taki sposób, że a≥0i b≥0pozostaje prawdziwe.

Rozszerzony algorytm euklidesowy

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

To powtórzenie kończy się, gdy b = 0, w którym to przypadku zmienne zawierają rozwiązanie tożsamości Bézouta : xA + yB = gcd(A,B) .

Sortowanie niedeterministyczne

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

Program ciągle permutuje elementy, podczas gdy jeden z nich jest większy niż jego następca. To niedeterministyczne sortowanie bąbelkowe nie jest bardziej wydajne niż jego deterministyczna wersja, ale jest łatwiejsze do udowodnienia: nie zatrzyma się, gdy elementy nie są posortowane i że w każdym kroku sortowane są co najmniej 2 elementy.

Argument maks.

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

Algorytm ten znajduje wartość 1 ≤ y ≤ n, dla której dana funkcja całkowita f jest maksymalna. Nie tylko obliczenia, ale także stan końcowy niekoniecznie są jednoznacznie określone.

Aplikacje

Programy poprawne konstrukcyjnie

Uogólnienie obserwacyjnej kongruencji strzeżonych poleceń w sieć doprowadziło do powstania rachunku udoskonalenia . Zostało to zmechanizowane w metodach formalnych, takich jak metoda B, które pozwalają formalnie wyprowadzać programy z ich specyfikacji.

Obwody asynchroniczne

Polecenia strzeżone nadają się do projektowania obwodów quasi-niewrażliwych na opóźnienia, ponieważ powtarzanie pozwala na dowolne względne opóźnienia przy wyborze różnych poleceń. W tej aplikacji bramka logiczna sterująca węzłem y w obwodzie składa się z dwóch strzeżonych poleceń, jak następuje: 

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

PullDownGuard i PullUpGuard są tutaj funkcjami wejść bramki logicznej, które opisują, kiedy bramka ściąga wyjście odpowiednio w dół lub w górę. W przeciwieństwie do klasycznych modeli oceny obwodów, powtórzenie zestawu strzeżonych poleceń (odpowiadające obwodowi asynchronicznemu) może dokładnie opisać wszystkie możliwe zachowania dynamiczne tego obwodu. W zależności od modelu, z jakim chcemy żyć dla elementów obwodu elektrycznego, dodatkowe ograniczenia dotyczące strzeżonych poleceń mogą być konieczne, aby opis strzeżonych poleceń był całkowicie zadowalający. Typowe ograniczenia obejmują stabilność, brak zakłóceń i brak samounieważniających poleceń.

Sprawdzanie modelu

Polecenia strzeżone są używane w języku programowania Promela , który jest używany przez kontroler modelu SPIN . SPIN weryfikuje poprawność działania współbieżnych aplikacji.

Inne

Moduł Perla Commands::Guarded implementuje deterministyczny, korygujący wariant strzeżonych poleceń Dijkstry.

Bibliografia

  1. ^ Dijkstra, Edsger W . „EWD472: Polecenia strzeżone, nieokreśloność i formalne wyprowadzanie programów” (PDF) . Pobrano 16 sierpnia 2006 .
  2. ^ Anne Kaldewaij (1990), Programowanie: wyprowadzenie algorytmów , Prentice Hall
  3. ^ Powrót Ralph J (1978). „O poprawności etapów udoskonalania w rozwoju programu (praca doktorska)” (PDF) . Zarchiwizowane z oryginału (pdf) w dniu 2011-07-20.
  4. ^ Martin, Alain J. „Synteza asynchronicznych obwodów VLSI” .