/* carre
 * Author: 
 * Creation date: 07/11/2019
 */
MACHINE
    carre
OPERATIONS
res <--    carreN (nn) =
PRE nn : NAT 
    & nn >= 1 
    & nn < MAXINT
    &  nn*nn <= MAXINT
THEN
    ANY rr WHERE
        rr : NAT 
    &   nn*nn <= MAXINT
    &   rr = nn*nn 
    THEN
        res := rr
    END
END   
;
res <-- carreZ (vv) = /* carre de Z */
PRE 
    vv : INTEGER
    & vv < MAXINT
    & vv*vv <= MAXINT
    THEN
    ANY rr WHERE
    rr : NATURAL 
    & rr = vv*vv
THEN
    res := rr
END
END

END