View article

Por lo general, un componente de software en un lenguaje orientado a objetos tiene requerimientos que no son simples de especificar cuando se trata del orden en que sus métodos pueden ser invocados. Generalmente sólo se provee documentación para cada método sin especificar cuál es el protocolo esperado de uso y la interacción entre los métodos, lo que puede llevar a usos inválidos. La minería de especificaciones, si provee información apropiada al programador, puede ayudar a mitigar estos problemas. Esto ha incentivado varias investigaciones de técnicas de inferencias de modelos que infieren un modelo basado en Finite State Machines (FSMs).

Actualmente existen herramientas capaces de analizar el código fuente en forma estática generando modelos que ayudan a contrastar la implementación con su especificación. Herramientas como Contractor crean un Labeled Transition System (LTS) específico llamado Enabledness Preserving Abstraction (EPA)[dCBGU11] a partir de una especificación por contratos o código fuente haciendo análisis estático.