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 necesaria ] El refinamiento paso a paso permite que este proceso se realice en etapas. Lógicamente, el refinamiento normalmente implica implicaciones , pero puede haber complicaciones adicionales.
La preparación progresiva justo a tiempo de la cartera de productos (lista de requisitos) en enfoques de desarrollo de software ágiles , 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 necesaria ] El refinamiento de operaciones convierte una especificación de una operación en un sistema en un programa implementable (por ejemplo, un procedimiento ). En este proceso se puede reforzar la poscondición y/o debilitar la precondición . 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 se puede implementar; es imposible seleccionar un miembro del conjunto vacío .
También se utiliza a veces el término cosificación (acuñado por Cliff Jones ). La reducción es una técnica alternativa cuando el refinamiento formal no es posible. 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 del programa. El Sistema de Transformación FermaT es una implementación de refinamiento de potencia industrial. El método B es también un método formal que amplía el cálculo de refinamiento con un lenguaje componente: se ha utilizado en desarrollos industriales.
En teoría de tipos , un tipo de refinamiento [2] [3] [4] es un tipo dotado de un predicado que se supone válido para cualquier elemento del tipo refinado. Los tipos de refinamiento pueden expresar condiciones previas cuando se usan como argumentos de función o condiciones posteriores cuando se usan 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 se puede escribir como . Los tipos de refinamiento están, por tanto, relacionados con los subtipos de comportamiento .
