• View
• Edit
• History
• Print

Lot

 SPECIFICATION choixdistant [inL,outL,inR,outR] : noexit

 library 
   BOOLEAN
 endlib 


 BEHAVIOUR
    entite  [inL,outL,inR,outR]

 WHERE
   PROCESS entite [insup,outsup,e,s] : noexit :=
	(*...completer*)
   ENDPROC


 TYPE Lesdonnee IS Boolean
   SORTS donnee,controle
   OPNS m (*! constructor *) : -> donnee
	ack (*! constructor *),
	token  (*! constructor *) : -> controle
	_eq_  : controle,controle -> Bool

   EQNS
	forall x,y : controle
	ofsort Bool
	ack eq ack = true;
	token eq token = true;
	ack eq token = false;
	token eq ack = false;


 ENDTYPE


 ENDSPEC