Reguła ramki jako preserver zmian?

Reguła rama , jak ten podany poniżej, oddaje ideę, że, biorąc pod uwagę program cz warunkiem p, że posiada zanim skończy i postcondition qktóra posiada potem jakiś warunek rozłączne rpowinny utrzymać zarówno przed jak i po cserii. ( *Łącznik wymaga, aby jego argumenty były rozłączne.) Często warunki wstępne i końcowe są stanami stosu i cjest to skuteczny program, który w pewien sposób modyfikuje stos.

    {p} c {q}
----------------- (where no free variable in r is modified by c)
{p * r} c {q * r}

Dyskusje na temat reguły ramki, którą widziałem, zawsze koncentrują się na tym, jak zachowana jest rozłączna część stosu r. Umożliwia to „lokalne rozumowanie”: gdy zastanawiamy się nad efektem c, możemy zignorować rczęść sterty i zajmować się tylko tą częścią, która faktycznie się zmienia. Ale innym sposobem na to jest to, że zmiana z pnaq została zachowana, mimo że rteraz tam jest. Innymi słowy, ważne jest, abyśmy skończyli z warunkiem {q * r}, a nie {q' * r}z innymi q'.

Moje pytanie brzmi więc, czy istnieje jakikolwiek sposób traktowania reguły ramowej, który omawia lub wykorzystuje zachowanie zachowania zmiany od rzeczy pdo qrzeczy.

Ale ta qwłaściwość „ bez zmian na własność” tak naprawdę nie obowiązuje!

Zastanów się {emp} x := alloc(0) {x |-> 0}. Teraz, jeśli wrobię y |-> 3, dostanę

{y |-> 3} x := alloc(0) {x |-> 0 * y |-> 3}

ale zgodnie z regułą mógłbym zmienić warunek na

{y |-> 3} x := alloc(0) {(x |-> 0 /\ x != y) * y |-> 3}

Aby uczynić to bardziej konkretnym, załóżmy, że yjest to liczba 37. Kiedy uruchomię komendę alokacji na całkowicie pustej stercie, możliwe jest, że skończę alokując adres 37, więc x = 37. Ale jeśli zacznę od stosu zawierającego pojedynczą komórkę pod adresem y = 37, wynik ten nie będzie już możliwy! Dodanie ramki do warunku wstępnego przycięło część niedeterminizmu w późniejszym stanie.

Artykuł „Lokalna logika działania i abstrakcyjna separacja” (Calcagno, O'Hearn i Yang) dotyczy zrozumienia reguły ramowej z głębszej, semantycznej perspektywy. Kluczową definicją artykułu jest lokalizacja dla „akcji”, gdzie akcja jest (semantyczną reprezentacją) programu. Lokalność mówi, że po dodaniu stosu ramek jedynym sposobem na zmianę pierwotnego warunku końcowego jest przycięcie jakiegoś niedeterminizmu, jak wyżej. W rzeczywistości przycinanie powstaje tylko z powodu alokacji.

Po pierwsze, w twoim pytaniu jest małe nieporozumienie, do czego Aaron doszedł również w swojej odpowiedzi. Predykaty w logice separacji są zbiorami hałd (lub równoważnie predykatami na hałdach), a koniunkcję oddzielającą definiuje się jako:$P \ast Q$

$$P \ast R \triangleq \{h_1 \cdot h_2 \;|\; h_1 \in P \;\wedge\; h_2 \in R \;\wedge\; \mathrm{dom}(h_1) \cap \mathrm{dom}(h_2) = \emptyset\}$$

Więc w regule ramki

$$\frac{\{P\}c\{Q\}}{\{P\ast R\}c\{Q \ast R\}}$$

(oraz P i Q ) nie mówią o konkretnych hałdach - sąwłaściwościamihałd (ponieważ podzbiory i predykaty są równoważne). Najlepszym sposobem na zrozumienie, co się dzieje, jest określenie, co oznacza trzymanie potrójnego Hoare:$R$$P$$Q$

$$\{P\}c\{Q\} \triangleq \forall h_1 \in P.\; \forall h' \in \mathrm{Heap}\;\mbox{s.t.}\; h' \# h_1.\;\exists h_2 \in Q.\; \left<h_1\cdot h'; c\right> \mapsto^\ast \left<h_2\cdot h'; \mathsf{skip}\right>$$

Ta definicja zasadniczo mówi, że (1) jeśli uruchomisz z dowolnym h 1 w P , to zakończysz w jakimś stanie końcowym h 2 w Q , i (2) jeśli dodasz jakąkolwiek dodatkową pamięć h ′ , pamięć ta będzie pozostać niezmienionym na końcu cyklu. Ale uwaga, że specyficzny h 2 dostać mogą się różnić dla różnych wyborów h ' --- co jest zagwarantowane jest, że właściwości P i Q nadal będzie trzymać pod tym idzie, nie, że masz dokładnie taki sam wynik sterty.$c$$h_1$$P$$h_2$$Q$$h'$ $h_2$$h'$ $P$$Q$

Nie jest to zbyt trudne, ale nadal warto poćwiczyć, aby zobaczyć, jak ta definicja potrójnego Hoarea sugeruje, że obowiązuje reguła ramki. Jak zauważasz, jest to rodzaj właściwości „zachowania zmian” i ma szczególnie żywe wyrażenie w stwierdzeniu reguły równoległego składu w logice separacji równoległej:

$$\frac{\{P_1\}c_1\{Q_1\} \qquad \{P_2\}c_2\{Q_2\}}{\{P_1 \ast P_2\}c_1 || c_2 \{Q_1 \ast Q_2\}}$$

Jeśli i c 2 działają na rozłączne regiony pamięci, to każdy z nich nie będzie zakłócał właściwości wykonywania drugiego, gdy są one uruchamiane równolegle.$c_1$$c_2$

Dyskusja na ten temat znajduje się w artykule Hoare i in., On Locality and the Exchange Law for Concurrent Processes , gdzie pokazują, jak dać połączoną algebrę programów i stwierdzeń.

Chociaż nie jest w 100% spokrewniony, ma smak idempotencji kontraktowej.

Jeśli myślimy o {p} jako warunku wstępnym na c, a {q} jako warunku dodatkowym na c, to idea reguły ramowej zapewniłaby, że warunki wstępne i końcowe będą obowiązywać w każdym kontekście obliczeniowym, a nie prosty przypadek, w którym nic innego nie istnieje.

To powiedziawszy, nie mogę powiedzieć, że widziałem taką regułę ramową przedstawioną w kilkudziesięciu dokumentach kontraktowych, które przeczytałem. Jest to z pewnością świetny pomysł, a wymaganie takiej zmiany może wiele zrobić w kierunku wypracowania rozsądnego, namacalnego zrozumienia idempotentnych umów.