Describir: Estudio de diversos metodos de especificacion formal de programas