W artykule „Bezkonfliktowy zreplikowany typ danych JSON” napotkałem ten zapis do formalnego definiowania „reguł”:
Jak nazywa się ten zapis? Jak to czytać?
Na przykład:
DOC
reguła nie ma nic w „liczniku” - dlaczego nie?- te
EXEC
iGET
zasady wydają się mieć dwa oddzielne terminy powyżej linii, co to znaczy? VAR
reguła wyróżnia się trochę, jak również, ponieważ podczas gdy wiele innych zasad użyć jakiegoś strzałką (który wziąłbym oznacza „implikuje”) do góry to tylko jeden zdaje się mówić, że x jest elementem czegoś.- prawie wszystko jest przesycone inicjałem,
Ap,
który tekst opisuje jako „stan repliki p jest opisany przez Ap, skończona funkcja częściowa” - jak bystry czytelnik tego zapisu miał tendencję do „dostrzegania” tej części każdej reguły?
Ta strona zasugerowała powiązane pytanie, które ma bardzo podobny wygląd, w odniesieniu do pytania Jakie jest znaczenie „B, s⟩ -> ⟨B”, s'⟩ jako początkowej reguły w tym pytaniu o małym kroku semantyka? - jest to oznaczone jako semantyka operacyjna i wydaje się, że jest to silny trop. Czy rzeczywiście są to ramy, w których powinienem interpretować te liczby? Czy mógłbyś łatwo streścić to w formie „kursu awaryjnego”, aby nawet jeśli nie mogę zweryfikować poprawności ich dowodów, mógłbym przynajmniej lepiej zrozumieć, co mówią w tej sekcji?
Oto bardzo nieformalne wyjaśnienie, które może pomóc osobom niezaznajomionym z formalnymi notacjami dostać się do drzwi. Nie zastępuje formalnej definicji!
Ap jest stan systemu lub programu z systemem. „Stan” może oznaczać wiele rzeczy, ale w tym przypadku wydaje się, że zawiera listę wszystkich zdefiniowanych zmiennych lokalnych i ich wartości. Dlaczego Ap jest funkcją? Ponieważ jest to wygodny sposób wyrażania przypisań zmiennych: Ap (x) podaje wartość zmiennej x .
Weźmy teraz za przykład regułę EXEC. Definiuje semantykę wykonywania polecenia cmd1, po którym następuje polecenie cmd2 , tj. Co dzieje się ze stanem Ap systemu podczas wykonywania cmd1, po którym następuje cmd2 .
Pozostałe reguły opisują semantykę poszczególnych poleceń i wyrażeń. Na przykład reguła VAR opisuje, co to znaczy „wykonać” zmienną: jeśli x jest zmienną lokalną (powyżej linii), co oznacza wycena / wykonanie zmiennej x ? Jest napisane poniżej linii: Gdy twój program jest w stanie Ap , ocena x daje ci wartość x , tj. Ap (x) .
Mam nadzieję że to pomogło.
źródło