Refinamiento es un término genérico de la informática que abarca varios enfoques para producir programas informáticos correctos y simplificar los programas existentes para permitir su verificación formal.
En los métodos formales , el refinamiento del programa es la transformación verificable de una especificación formal abstracta (de alto nivel) en un programa ejecutable concreto (de bajo nivel) . [ cita requerida ] El refinamiento paso a paso permite que este proceso se realice por etapas. Lógicamente, el refinamiento normalmente implica implicación , pero puede haber complicaciones adicionales.
La preparación progresiva justo a tiempo de la cartera de productos (lista de requisitos) en enfoques ágiles de desarrollo de software , como Scrum , también se describe comúnmente como refinamiento. [1]
El refinamiento de datos se utiliza para convertir un modelo de datos abstracto (en términos de conjuntos, por ejemplo) en estructuras de datos implementables (como matrices ). [ cita requerida ] El refinamiento de operaciones convierte una especificación de una operación en un sistema en un programa implementable (por ejemplo, un procedimiento ). La postcondición puede fortalecerse y/o la precondición debilitarse en este proceso. Esto reduce cualquier no determinismo en la especificación, típicamente a una implementación completamente determinista .
Por ejemplo, x ∈ {1,2,3} (donde x es el valor de la variable x después de una operación) podría refinarse a x ∈ {1,2}, luego x ∈ {1} e implementarse como x : = 1. Las implementaciones de x := 2 y x := 3 serían igualmente aceptables en este caso, usando una ruta diferente para el refinamiento. Sin embargo, debemos tener cuidado de no refinar a x ∈ {} (equivalente a falso ) ya que esto no es implementable; es imposible seleccionar un miembro del conjunto vacío .
El término reificación también se usa a veces (acuñado por Cliff Jones ). La reducción es una técnica alternativa cuando no es posible el refinamiento formal. Lo opuesto al refinamiento es la abstracción .