3 maneras de modelar el conjunto de números pares no negativos
Original web-page: http://xfront.com/Alloy/3-ways-to-model-the-set-of-non-negative-even-numbers.html
Roger L. Costello
Introducción
He aquí por qué creo que debería leer este documento:
- Eso demuestra que Alloy y Alloy es realmente útil. Se utiliza con eficacia, la Alloy puede ayudar a crear un software mejor, más fiable.
- Este papel es corto y fácil de leer y le dará una buena idea de lo que puede hacer con la Alloy.
Aquí está el lado negativo de este trabajo: Lo que se está modelando – el conjunto de los números pares no negativos – no es interesante, ni es típica de las cosas que normalmente modelo con Alloy. Alloy se suele utilizar para modelar software y/o sistemas.
A pesar de la desventaja, siento que este trabajo es bastante útil y vale la pena leer.
Vamos a suponer que usted todavía está leyendo, así que vamos a comenzar con una visión general de lo que se verá en este documento.
Este documento muestra 3 maneras diferentes para modelar el conjunto de números pares no negativos. Muestra cómo se puede obtener un mayor nivel de seguridad de que su modelo es correcto al especificar y comprobar algunas propiedades que definen. Por último, se muestra cómo se puede comprobar si dos modelos diferentes son equivalentes.
Planteamiento del problema: representar de manera concisa (modelo) de este ejemplo: 0, 2, 4, …
Lista modelo
Comencemos simple. En lugar de modelar una lista infinita, modelemos esta lista finita: 0, 2, 4, 6.
Aquí está el modelo de Alloy:
one sig List {
numbers: set Int
}{
numbers = 0 + 2 + 4 + 6
}
sig es una palabra reservada. Se encuentra a la firma. Una declaración de la firma define un conjunto. En este caso, la declaración de la firma define un conjunto con nombre de lista. El conjunto tiene un solo miembro. Se puede pensar en la lista como un objeto (en el sentido orientado a objetos). El objeto tiene un campo llamado números. Se llevará a cabo la lista deseado de valores (0, 2, 4, 6). El valor de los números es un conjunto de números enteros (int).
Sin embargo, no queremos que el valor de los números para contener cualquier conjunto de números enteros de edad. Queremos que contiene solo los números enteros 0, 2, 4, 6. Por lo tanto, complementaria de la Declaración de la firma con un hecho de la firma que contrains el conjunto. (El hecho de la firma es la materia en el segundo par de llaves) El símbolo más (+) no significa, además, que significa unión de conjuntos. En la Alloy de cada valor es un conjunto, por ejemplo, 0 es {0}, 1 es {1} y 0 + 1 es {0, 1}. Por lo tanto, el valor de los números es el conjunto deseado.
Modelo predicado
La notación de lista solo se puede utilizar para modelar conjuntos finitos. La notación de predicado se puede utilizar para modelar conjuntos infinitos.
El enfoque adoptado por la notación de predicado es representar un conjunto especificando las propiedades que debe tener cada miembro del conjunto. En nuestro caso, cada entero en el conjunto debe tener estas dos propiedades:
- El entero debe ser par.
- El entero no debe ser negativo.
Estos se llaman “propiedades definitorias”.
Aquí está el modelo de Alloy:
one sig List {
numbers: set Int
}{
numbers = {i: Int | i >= 0 and (rem[i,2] = 0)}
}
El hecho de firma utiliza una comprensión conjunto para especificar el valor de números: el conjunto de todos entero i tal que i es mayor que o igual a 0 y el resto de la división i por 2 es 0.
Modelo del generador
Supongamos que existe un modelo de una recta numérica en la que cada entero i está conectado a i+2
Luego, el conjunto deseado de enteros se puede modelar como: La cadena de enteros que comienza en 0.
Es mejor modelar la recta numérica como una secuencia en la que cada entero i tiene i.next e i.prev en lugar de i+1 y i-1. He aquí por qué: dado que las computadoras son finitas, las instancias también son finitas. Las instancias modeladas agregando 2 a cada entero eventualmente fallarán con un desbordamiento aritmético o con una adición alrededor de valores negativos. Entonces, en lugar de que la instancia conecte i con i+2, la instancia conecta i con el entero que está a dos pasos de la secuencia: i.next.next
Aquí está el modelo de Alloy:
one sig NumberLine {
connections: Int -> Int
} {
all i: Int | connections[i] = i.next.next
}
La declaración de la firma define NumberLine, que tiene un campo llamado conexiones. El valor de las conexiones es un conjunto de (int, int) pares. El operador flecha (->) significa “todas las combinaciones posibles del conjunto de la izquierda de la flecha con el juego a la derecha de la flecha.” Usted puede recordar de su clase de matemáticas de la escuela secundaria que esto se llama el producto cartesiano.
Sin embargo, no queremos que el valor de las conexiones sean todos los pares posibles (int, int). Solo queremos (i, i.next.next) pares. El hecho de la firma restringe los pares: para todos los enteros i, el valor de la ithth connection es i.next.next
Ahora que la línea numérica está definida, estamos listos para modelar la lista deseada. El valor de los números es la cadena que comienza en 0.
one sig List {
numbers: set Int
} {
numbers = 0.*(NumberLine.connections)
}
El operador clausura transitiva reflexiva (*) significa “en un conjunto de pares, siempre que haya un par (A, B) y un par (B, C), a continuación, añadir estos pares: (A, A) y (A, C)”. En otras palabras, crear pares para todos los valores que A puede alcanzar, incluida la propia. Para nuestro caso, el conjunto de pares contiene (0, 2) y (2, 4), por lo que el operador * añadirá estos pares: (0, 0) y (0, 4).
0.*(NumberLine.connections) significa “todos los enteros que se pueden alcanzar desde 0,” cual es: 0, 2, 4, 6, …
Para aumentar el nivel de confianza de que este modelo genera una instancia con la lista de enteros deseada, podemos verificar que cada entero en números tenga las dos propiedades de definición que vimos anteriormente:
- Propiedad par: cada entero debe ser par.
- Propiedad no negativa: cada entero debe ser no negativo.
La Alloy aserción se utiliza para comprobar un modelo. Las siguientes comprobaciones afirmar que cada número entero en números tiene las dos propiedades que definen:
assert only_positive_even_numbers {
all i: List.numbers | i >= 0 and rem[i, 2] = 0
}
Lea como: Para todos los números i en números de Lista, i debe ser mayor o igual a 0 y el resto de la división de i por 2 debe ser cero.
Cuando se le solicita al Analizador de Aleaciones que verifique la afirmación, responde con “No se ha encontrado ningún contraejemplo”. En otras palabras, Alloy Analyzer no puede encontrar un miembro de números que no sea negativo y/o que no sea par.
Equivalencia de los modelos de predicado y el generador
El modelo de predicado representa de manera concisa (modelos) la lista: 0, 2, 4, 6, … El modelo de generador también representa (modelos) de manera concisa la lista: 0, 2, 4, 6, … Nos gustaría mostrar que los dos modelos son equivalentes es decir, ambos representan (modelan) la misma instancia.
A continuación se muestran los dos modelos y una afirmación que prueba su equivalencia. Observe que el hecho de la firma para la firma de la Lista se ha ido. En cambio, hay dos pred (predicados). El nombre predicho Predicate, cuando se invoca, restringe los números mediante un conjunto de comprensión. Cuando se invoca el generador de predatos, cuando se invoca, restringe los números a la cadena de números enteros en NumberLine a partir de 0. También observe que en cada predio el campo de los números está calificado explícitamente con “Lista” para indicar que los números son un campo dentro de la Lista. Anteriormente, cuando se usaba un hecho de firma, la “Lista” estaba implícita. En la parte inferior hay una afirmación. Dice esto: si una instancia satisface las restricciones especificadas en Predicate, la instancia también satisfará las restricciones especificadas en Generator, y viceversa. En otras palabras, la instancia representada por Predicate es la misma instancia representada por Generator. Cuando se le solicita al Analizador de Aleaciones que verifique la afirmación, responde con “No se ha encontrado ningún contraejemplo”. En otras palabras, el modelo de Predicado y el modelo de Generador son equivalentes. Muy genial.
Aquí está el modelo de Alloy:
one sig NumberLine {
connections: Int -> Int
} {
all i: Int | i.connections = i.next.next
}
one sig List {
numbers: set Int
}
pred Predicate {
List.numbers = {i: Int | i >= 0 and (rem[i,2] = 0)}
}
pred Generator {
List.numbers = 0.*(NumberLine.connections)
}
assert Equivalent {
Predicate iff Generator
}
Roger L. Costello. 18 de abril de 2018
Recent Comments