CHOIX /
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