Cientifico

ORIENTADOS A OBJETOS

Un MFOO es un conjunto de técnicas de modelado para especificar, desarrollar y verificar sistemas software mediante el uso del lenguaje matemático y características orientadas a objetos.

Por sistema software orientado a objetos se entiende, de forma general, a toda colección de objetos que colaboran entre sí para conseguir un propósito (objetivos del sistema software).

Muchos de los métodos formales presentes en la literatura aparecen como métodos formales extendidos con conceptos de orientación a objetos. Es decir, la existencia de un lenguaje formal suele ser previa a la existencia del lenguaje orientado a objetos.

Este hecho ha condicionado en gran medida las diferentes propuestas y así queda reflejado en el presente documento.

Dada la diversidad de trabajos y formalismos existentes en la actualidad, es necesario establecer qué se entiende por formal y qué se entiende por orientación a objetos. El término formal queda caracterizado por la categoría de modelos matemáticos utilizados. Ejemplos de formalismos son: lógica de primer orden, álgebras, redes de Petri y lógica temporal. Por otra parte, el término orientado a objeto queda caracterizado por los conceptos de objeto, ocultación, interacción, abstracción, concurrencia, clase, herencia, (sub)tipo y genericidad.

Los formalismos basados en lógica de primer orden y teoría de conjuntos [MaW85] permiten especificar el sistema mediante un concepto formal de estado y operaciones sobre estados. Con este propósito, datos y relaciones/funciones se describen en detalle y sus propiedades se expresan en lógica de primer orden. La semántica de los lenguajes está basada en la teoría de conjuntos.

Durante el diseño e implementación del sistema, los elementos descritos matemáticamente pueden modificarse preservando las características esenciales de la especificación inicial.

Los formalismos algebraicos proponen la descripción de estructuras de datos estableciendo el nombre de los diferentes conjuntos de datos, funciones básicas y propiedades. No hay concepto de estado modificable en el tiempo. Las propiedades se describen mediante fórmulas, generalmente, ecuaciones.

Diferentes modelos semánticos se han propuesto para caracterizar las especificaciones algebraicas: modelos iniciales, finales y laxos.

Los modelos iniciales identifican términos cuya igualdad puede ser probada desde los axiomas. Los modelos finales identifican términos diferentes cuya desigualdad puede ser probada desde sus axiomas y los modelos laxos identifican todas las álgebras cuyos elementos pueden denotarse con términos sin variables. Para describir sistemas (de estructuras de datos) se propone una amplia gama de operadores de composición y parametrización.

Un conocimiento de sistema resulta necesario

...