Langage de commande protégé - Guarded Command Language

Le Guarded Command Language ( GCL ) est un langage défini par Edsger Dijkstra pour la sémantique des transformateurs de prédicats . Il combine les concepts de programmation de manière compacte, avant que le programme ne soit écrit dans un langage de programmation pratique. Sa simplicité permet de prouver plus facilement l'exactitude des programmes, en utilisant la logique de Hoare .

Commandement gardé

La commande gardée est l'élément le plus important du langage de commande gardé. Dans une commande gardée, comme son nom l'indique, la commande est "gardée". La garde est une proposition , qui doit être vraie avant que l'instruction ne soit exécutée . Au début de l'exécution de cette instruction, on peut supposer que la garde est vraie. De plus, si la garde est fausse, l'instruction ne sera pas exécutée. L'utilisation de commandes protégées permet de prouver plus facilement que le programme répond aux spécifications . La déclaration est souvent une autre commande gardée.

Syntaxe

Une commande gardée est une instruction de la forme G → S, où

• G est une proposition , appelée la garde
• S est une déclaration

Si G est vrai, la commande gardée peut être écrite simplement S.

Sémantique

Au moment où G est rencontré dans un calcul, il est évalué.

• Si G est vrai, exécutez S
• Si G est faux, regardez le contexte pour décider quoi faire (dans tous les cas, n'exécutez pas S)

Ignorer et abandonner

Skip et Abort sont des instructions très simples et importantes dans le langage de commande protégé. Abandonner est l'instruction indéfinie : faire n'importe quoi. L'instruction abort n'a même pas besoin de se terminer. Il est utilisé pour décrire le programme lors de la formulation d'une preuve, auquel cas la preuve échoue généralement. Skip est l'instruction vide : ne rien faire. Il est utilisé dans le programme lui-même, lorsque la syntaxe requiert une instruction, mais que le programmeur ne souhaite pas que la machine change d' état .

Syntaxe

skip

abort

Sémantique

• Passer : ne rien faire
• Abandonner : faire n'importe quoi

Mission

Affecte des valeurs aux variables .

Syntaxe

v := E

ou

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

où

• v sont des variables de programme
• E sont des expressions du même type de données que leurs variables correspondantes

Enchaînement

Les instructions sont séparées par un point-virgule (;)

Sélection : si

La sélection (souvent appelée "instruction conditionnelle" ou "instruction if") est une liste de commandes protégées, dont une est choisie pour être exécutée. Si plus d'une garde est vraie, une instruction est choisie de manière non déterministe pour être exécutée. Si aucune des gardes n'est vraie, le résultat est indéfini. Parce qu'au moins une des gardes doit être vraie, l'instruction vide "sauter" est souvent nécessaire.

Syntaxe

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

Sémantique

Lors de l'exécution d'une sélection, toutes les gardes sont évaluées. Si aucune des gardes n'est évaluée à vrai, l'exécution de la sélection s'interrompt, sinon l'une des gardes qui a la valeur vraie est choisie de manière non déterministe et l'instruction correspondante est exécutée.

Exemples

Simple

En pseudo - code :

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

En langage de commande gardé :

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

Utilisation de sauter

En pseudo-code :

if error is True then 
  set x to 0

En langage de commande gardé :

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

Si la deuxième garde est omise et que error = False, le résultat est annulé.

Plus de gardes vrai

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

Si a = b, a ou b est choisi comme nouvelle valeur pour le maximum, avec des résultats égaux. Cependant, quelqu'un qui l' implémente peut trouver que l'un est plus facile ou plus rapide que l'autre. Puisqu'il n'y a aucune différence pour le programmeur, il est libre d'implémenter l'une ou l'autre manière.

Répétition : faire

La répétition exécute les commandes gardées à plusieurs reprises jusqu'à ce qu'aucune des gardes ne soit vraie. Habituellement, il n'y a qu'un seul gardien.

Syntaxe

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

Sémantique

Lors de l'exécution d'une répétition, toutes les gardes sont évaluées. Si toutes les gardes sont évaluées à faux, alors skip est exécuté. Sinon, l'une des gardes qui a la valeur true est choisie de manière non déterministe et l'instruction correspondante est exécutée après quoi la répétition est exécutée à nouveau.

Exemples

Algorithme euclidien original

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

Cette répétition se termine lorsque a = b, auquel cas a et b ont le plus grand commun diviseur de A et B.

Dijkstra voit dans cet algorithme un moyen de synchroniser deux cycles infinis a := a - bet b := b - ade telle sorte que a≥0et b≥0reste vrai.

Algorithme euclidien étendu

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

Cette répétition se termine lorsque b = 0, auquel cas les variables contiennent la solution de l'identité de Bézout : xA + yB = pgcd(A,B) .

Tri non déterministe

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

Le programme continue de permuter des éléments alors que l'un d'entre eux est supérieur à son successeur. Ce tri à bulles non déterministe n'est pas plus efficace que sa version déterministe, mais plus facile à prouver : il ne s'arrêtera pas tant que les éléments ne sont pas triés et qu'à chaque étape il trie au moins 2 éléments.

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

Cet algorithme trouve la valeur 1 ≤ y ≤ n pour laquelle une fonction entière donnée f est maximale. Non seulement le calcul mais aussi l'état final ne sont pas nécessairement déterminés de manière unique.

Applications

Programmes corrects par construction

La généralisation de la congruence observationnelle des commandes gardées dans un réseau a conduit au calcul de raffinement . Cela a été mécanisé dans des méthodes formelles comme la méthode B qui permettent de dériver formellement des programmes à partir de leurs spécifications.

Circuits asynchrones

Les commandes gardées conviennent à la conception de circuits quasi insensibles aux retards car la répétition autorise des retards relatifs arbitraires pour la sélection de différentes commandes. Dans cette application, une porte logique pilotant un nœud y dans le circuit se compose de deux commandes gardées, comme suit :

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

PullDownGuard et PullUpGuard ici sont des fonctions des entrées de la porte logique, qui décrivent quand la porte tire la sortie vers le bas ou vers le haut, respectivement. Contrairement aux modèles d'évaluation de circuit classiques, la répétition d'un ensemble de commandes gardées (correspondant à un circuit asynchrone) peut décrire avec précision tous les comportements dynamiques possibles de ce circuit. Selon le modèle avec lequel on est prêt à vivre pour les éléments de circuit électrique, des restrictions supplémentaires sur les commandes gardées peuvent être nécessaires pour qu'une description de commande gardée soit entièrement satisfaisante. Les restrictions courantes incluent la stabilité, la non-interférence et l'absence de commandes d'auto-invalidation.

Vérification de modèle

Les commandes protégées sont utilisées dans le langage de programmation Promela , qui est utilisé par le vérificateur de modèle SPIN . SPIN vérifie le bon fonctionnement des applications logicielles concurrentes.

Autre

Le module Perl Commands::Guarded implémente une variante déterministe et rectificatrice des commandes gardées de Dijkstra.

Les références