IMPLEMENTATION
	euclide_I1_1
REFINES
	euclide

OPERATIONS
	
	
reste, quot <-- calculReste(divis, divid) = 
	VAR rr, mm, dd IN 
	  dd := 0         /* le  multiple de divis */
	; mm := dd*divis  
	; rr := divid     /* le reste courant */
	;
        WHILE         /* Maintenant, calcul du reste par soustractions successives 
			des multiples de mm */
	    rr <= divis & dd + 1  < MAXINT
	DO
		dd := dd + 1
	;	rr := rr - divis
	INVARIANT
	     0 <= rr 
	&    dd : NAT
	&    rr : NAT
	&    dd+1 < MAXINT
	&    divid = mm*dd +rr /*  &  $\exists$ dd | divid = divis*dd + rr */
	VARIANT
	     rr-divis      /* décroit jusqu'a */
	END
	;       reste := rr
	;	quot:= dd
	END
END

/* 3 preuves non dechargees 

 dd$0+1+1+1<=2147483647 
 0*divis*dd$0+rr$0 = 0*divis*(dd$0+1)+(rr$0-divis)
 0*divis*dd$7777+rr$7777 = dd$7777*divis+rr$7777 
*/


/*------------------------Version abstraite
 reste, quot <-- calculReste (divis, divid) = 
 PRE
	 divis : NAT
 &  	divid : NAT  
 &  	divis > 0
 THEN 
 	ANY vq, vr WHERE
	 	vq  : NAT
	& 	vr  : NAT
	& 	divid = vq*divis + vr
	THEN 
	 	quot  :=  vq 
	|| 	reste  :=  vr 
 	END
 END
-------------------------------
*/