Refinamiento (informática) - Refinement (computing)

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.

Refinamiento del programa

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) . El refinamiento gradual 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 acumulación de productos (lista de requisitos) en enfoques de desarrollo de software ágiles , como Scrum , también se describe comúnmente como refinamiento.

Refinamiento de datos

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 ). El refinamiento de la operación convierte una especificación de una operación en un sistema en un programa implementable (por ejemplo, un procedimiento ). El postcondition se puede reforzar y / o la condición previa debilitado 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 ax ∈ {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 ax ∈ {} (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 .

Cálculo de refinamiento

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 fuerza 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.

Tipos de refinamiento

En la teoría de tipos , un tipo de refinamiento es un tipo dotado de un predicado que se supone que es 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 puede escribirse como . Por tanto, los tipos de refinamiento están relacionados con la subtipificación conductual . ${\ Displaystyle f: \ mathbb {N} \ rightarrow \ {n: \ mathbb {N} \, | \, n> 5 \}}$

Ver también

• Reificación (informática)

Referencias

Este artículo relacionado con la ingeniería de software es un código auxiliar . Puedes ayudar a Wikipedia expandiéndolo . v t mi