The factorial function

MACHINE
Factorielle
/*encapsule la fonction factorielle */
CONSTANTS
laFactorielle
PROPERTIES
laFactorielle : NAT --> NAT &
laFactorielle (0) = 1 &
! nn. (nn: NAT1 => laFactorielle (nn) = nn * laFactorielle (nn-1))
END

MACHINE
MaFactorielle
SEES
Factorielle
/* cette machine offre une operation qui appelle la fonction factorielle en lui passant le nombre dont on veut la factorielle. C'est une application de fonction */
OPERATIONS
reponse <-- fact(nn) =
PRE
nn : NAT
THEN
reponse := laFactorielle(nn)
END
END