El 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 de un 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 por pasos permite que este proceso se realice en etapas. Lógicamente, el refinamiento normalmente implica implicación , pero puede haber complicaciones adicionales.
La preparación progresiva justo a tiempo del product backlog (lista de requisitos) en enfoques de desarrollo de software ágil , 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 condición posterior se puede fortalecer y/o la condición previa se puede debilitar 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, utilizando una ruta diferente para el refinamiento. Sin embargo, debemos tener cuidado de no refinar a x ∈ {} (equivalente a false ) ya que esto no es implementable; es imposible seleccionar un miembro del conjunto vacío .
A veces también se utiliza el término cosificación (acuñado por Cliff Jones ). El retraimiento es una técnica alternativa cuando no es posible el refinamiento formal. Lo opuesto al refinamiento es la abstracción .
El cálculo de refinamiento es un sistema formal (inspirado en la lógica de Hoare ) que promueve el refinamiento de programas. El sistema de transformación de FermaT es una implementación de refinamiento de nivel industrial. El método B también es un método formal que extiende el cálculo de refinamiento con un lenguaje de componentes: se ha utilizado en desarrollos industriales.
En la teoría de tipos , un tipo de refinamiento [2] [3] [4] es un tipo dotado de un predicado que se supone que se cumple para cualquier elemento del tipo refinado. Los tipos de refinamiento pueden expresar condiciones previas cuando se utilizan como argumentos de función o condiciones posteriores cuando se utilizan como tipos de retorno : por ejemplo, el tipo de una función que acepta números naturales y devuelve números naturales mayores que 5 puede escribirse como . Por lo tanto, los tipos de refinamiento están relacionados con la subtipificación conductual .
