Describir: Métodos formales ligeros : especificación de un sistema de correo electrónico en el analizador Alloy