Condescending third world kid

Lenguaje de especificación de Alloy
MeFIS

2

Repaso sesión anterior
•  Relaciones
•  •  •  •  Composición de relaciones, inversa Cerradura reflexiva, transitiva, simétrica Restricción dedominio y de rango “Overriding”

3

Objetivos
•  Conocer la sintaxis y el significado de las construcciones básicas del lenguaje de especificación de Alloy •  Aprender a elaborarespecificaciones elementales en Alloy •  Manejar el ambiente de edición y verificación de Alloy
4

Tema de hoy
•  Lenguaje de especificación •  Actividades previas:
•  Estudio del tutorial de Alloy, primeraparte •  Examen previo

5

Ubicación del lenguaje
Conjuntos

Alloy

6

Ejemplo relaciones familiares
•  Queremos…
•  Modelar relaciones padre/hijo como relaciones primitivas •  Modelarrelaciones de esposos como primitivas •  Modelar relaciones tales como “hermano” como relaciones derivadas

7

Ejemplo relaciones familiares
•  Queremos…
•  Asegurar ciertas restriccionesbiológicas con predicados de 1er orden (p.ej., solo una madre) •  Asegurar ciertas restricciones sociales (p.ej., una esposa no es un hermano) •  Confirmar o refutar la existencia de relaciones derivadas,p.ej., nadie tiene una esposa con quien comparte un padre)

8

Construcción básica: Dominios
• 

Dominios son conjuntos básicos
• 
•  • 

Tienen elementos homogéneos Son disjuntosRepresentan los objetos individuales que son modelados Ejemplo: sig Person {}

• 

Los dominios se declaran en “signatures”
• 

9

“Signature” con atributos
sig Person { father: Person, mother:Person, child: Person, sibling: Person } father : Person -> Person mother : Person -> Person child : Person -> Person sibling : Person -> Person

10

Conjuntos como resultado
sig Person {father: Person, mother: Person, children: set Person, siblings: set Person } father : Person -> Person mother : Person -> Person children : Person -> set Person siblings : Person -> set Person

11...