 | Este artículo necesita citas adicionales para su verificación . ( septiembre de 2010 ) ( Aprenda cómo y cuándo eliminar este mensaje de plantilla ) |
| Transformación de datos |
|---|
| Conceptos |
| Lenguajes de transformación |
| Técnicas y transformaciones |
| Aplicaciones |
| Relacionados |
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 [ editar ]
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 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. [1]
Refinamiento de datos [ editar ]
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 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 el refinamiento formal no es posible. Lo opuesto al refinamiento es la abstracción .
Cálculo de refinamiento [ editar ]
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 [ editar ]
En la teoría de tipos , un tipo de refinamiento [2] [3] [4] 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 .
Ver también [ editar ]
- Reificación (informática)
Referencias [ editar ]
- ^ Cho, L (2009). "Adoptando una cultura ágil El viaje de un equipo de experiencia de usuario". Conferencia ágil : 416. doi : 10.1109 / AGILE.2009.76 . ISBN 978-0-7695-3768-9.
- ^ Freeman, T .; Pfenning, F. (1991). "Tipos de refinamiento para ML" (PDF) . Actas de la Conferencia ACM sobre diseño e implementación de lenguajes de programación . págs. 268-277. doi : 10.1145 / 113445.113468 .
- ^ Hayashi, S. (1993). "Lógica de tipos de refinamiento". Actas del Taller sobre Tipos de Pruebas y Programas . págs. 157-172. CiteSeerX 10.1.1.38.6346 . doi : 10.1007 / 3-540-58085-9_74 .
- ^ Denney, E. (1998). "Tipos de refinamiento para especificación". Actas de la Conferencia Internacional IFIP sobre Conceptos y Métodos de Programación . 125 . Chapman y Hall. págs. 148-166. CiteSeerX 10.1.1.22.4988 .
