/*--------------------------------------------
  NaBLa Project - LINA / University de Nantes 
  Euclide
  Correct Program Development
  Christian Attiogbe
----------------------------------------------*/
MACHINE 
	euclide

OPERATIONS

 reste, quot <-- calculReste (divis, divid) = 
 PRE
	 divis : NAT
 &  	divid : NAT  
 &  	divis > 0
 &      divis <= divid /* sinon b le trouve */
 &      divis <= MAXINT
 & divid <= MAXINT
 THEN 
 	ANY vq, vr WHERE
	 	vq  : NAT
	& 	vr  : NAT
	&       vq*divis + vr <= MAXINT
	& 	divid = vq*divis + vr
	&       vr < divis
	THEN 
	 	quot  :=  vq 
	|| 	reste  :=  vr 
 	END
 END


END