En el documento "Un tipo de datos JSON replicado libre de conflictos" , encontré esta notación para definir formalmente "reglas":
¿Cómo se llama esta notación? ¿Cómo lo leo?
Por ejemplo:
- el
DOC
regla no tiene nada en su "numerador", ¿por qué no? - Las reglas
EXEC
yGET
parecen tener dos términos separados sobre la línea, ¿qué significa eso? - la
VAR
regla también se destaca un poco, ya que si bien muchas otras reglas usan algún tipo de flecha (lo que supongo que significa "implica"), esta parece indicar que x es un elemento de algo. - Casi todo está salpicado de una inicial
Ap,
que el texto describe como "el estado de la réplica p es descrito por Ap, una función parcial finita". ¿Cómo un lector inteligente de esta notación tenderá a "ver" esa parte de cada regla?
Este sitio sugirió una pregunta relacionada que tiene una notación de aspecto muy similar, sobre la pregunta ¿Cuál es el significado de ⟨B, s⟩ -> ⟨B ', s'⟩ como la regla inicial en esta pregunta sobre pequeños pasos ¿semántica? - esto está etiquetado como semántica operacional , y eso parece ser una fuerte ventaja. ¿Es ese el marco en el que debería interpretar estas cifras? ¿Podría resumir esto fácilmente en forma de "curso intensivo" para que, incluso si no puedo verificar la exactitud de sus pruebas, al menos pudiera comprender un poco más lo que dicen en esta sección?
Aquí hay una explicación muy informal que podría ayudar a las personas que no están familiarizadas con las anotaciones formales a poner un pie en la puerta. ¡No reemplaza una definición formal!
El Ap es el estado de su sistema o su programa en ejecución. "Estado" puede significar muchas cosas, pero en este caso parece incluir una lista de todas las variables locales definidas y sus valores. ¿Por qué es Ap una función? Porque esa es una manera conveniente de expresar asignaciones de variables: Ap (x) da el valor de la variable x .
Ahora, tomemos la regla EXEC como ejemplo. Define la semántica de ejecutar un comando cmd1 seguido de un comando cmd2 , es decir, qué sucede con el estado Ap del sistema cuando se ejecuta cmd1 seguido de cmd2 .
Las otras reglas describen la semántica de los comandos y expresiones individuales. Por ejemplo, la regla VAR describe lo que significa "ejecutar" una variable: si x es una variable local (por encima de la línea), entonces, ¿qué significa evaluar / ejecutar la variable x ? Está escrito debajo de la línea: cuando su programa está en estado Ap , la evaluación de x le da el valor de x , es decir, Ap (x) .
Espero que eso ayude.
fuente