TP de langage de spécification

Partie 3

Créer une machine B pour représenter un file de voitures. On suposera que la route est constituée de cases successives indicées par ℤ. Il suffira donc de stocker l’ensemble des cases occupées par une voiture. Les voitures avancent dans le sens positif.

• Écrire une opération avance qui fait avancer la voiture située à la case passée en paramètre d’une case, en mettant en pré-condition que la case contient une voiture et que la case devant est vide (exemple : flèche rouge).
• Écrire une opération avanceNondeterministe qui fait avancer une voiture (n’importe laquelle) d’une case ou ne fait rien si aucune voiture ne peut avancer. Remarque : ça n’est possible que s’il y a une infinité de voitures.
• Écrire une opération double qui fait doubler une voiture (n’importe laquelle). C’est possible quand une voiture a une case occupée devant elle mais que la case suivante est vide (exemple: flèche verte)