Dlaczego stan pozostaje niezmieniony w niewielkiej semantyce operacyjnej pętli while?

9

Zwykle widzę, że w strukturalnej reprezentacji operacyjnej semantyki dla pętli while stan programu nie zmienia się:

$(while \> B \> do \>S, \sigma) \rightarrow (if \>B \> then \>S; (while \> B \> do \>S) \> else \> SKIP, \sigma)$

Dla mnie nie jest to intuicyjne, jeśli stan się nie zmieni (tzn. Stan pamięci pozostanie taki sam), wówczas pozostanie prawdą, a program nigdy się nie zakończy. $B$

Czy ktoś może wyjaśnić, dlaczego stan nie zmienia się w tej regule?

formal-languages programming-languages formal-methods operational-semantics El Marce
źródło

Zauważ, że jest to poprawne tylko wtedy, gdy możemy założyć, że

B

$B$ nie ma skutków ubocznych. Nie dotyczy to większości języków programowania.

Raphael

10

W semantyce języka programowania pojęcie stanu programu nie jest niejasnym pojęciem filozoficznym, ale bardzo precyzyjnym pojęciem matematycznym. Stanu w tym małym kroku semantyki operacyjnych jest częściowo funkcją $s$

s : V a r ↪ Z

$s : \mathbf{Var} \hookrightarrow \mathbb{Z}$

która rejestruje wartości zmiennych. Więc jeśli , to zmienna ma wartość . Stan jest koniecznie funkcją częściową, ponieważ sensowne jest jedynie rejestrowanie wartości zmiennych, które faktycznie występują. $s\, x = v$ $x$ $v$

Rozwijający się aksjomat

⟨ while b do S, s ⟩ \Rightarrow ⟨ if b then S; while b do S else skip, s ⟩

$\langle \texttt{while}\; b\; \texttt{do}\; S,s \rangle \Rightarrow \langle \texttt{if}\; b\; \texttt{then}\; S; \texttt{while}\; b\; \texttt{do}\; S \; \texttt{else skip},s \rangle$

po prostu mówi nam, że rozwijamy pętlę while w instrukcji warunkowej, której jedna gałąź zawiera pętlę. Z tego powodu żadne zmienne nie zmienią swojej wartości iz tego powodu stan się nie zmienia.

Hans Hüttel
źródło

10

Stan może się zmieniać w kolejnych krokach redukcji, ponieważ po prawej stronie

⟨ w h i l e B d o S, σ ⟩ \to ⟨ i f B t h e n (S; w h i l e B d o S) e l s e s k i p, σ ⟩

$\langle while\ B\ do\ S, \sigma \rangle \quad\rightarrow\quad \langle if\ B\ then\ ( {\color{red}{S}};\ while\ B\ do\ S )\ else\ skip, \sigma\rangle$

-loop jest chroniony (poprzedza) przez . Obliczenie może zmienić stan, aby warunek mógł zostać oceniony na . $while$ $S$ $S$ $B$ $\mathsf{false}$

Martin Berger
źródło

Oznacza to zatem, że zmianę stanu należy wyrazić w innych regułach, do których S można potencjalnie ograniczyć w konkretnym programie?

El Marce

@ElMarce Tak. Sugeruję przejść przez prosty przykład, np. i zobaczyć, jak to działa.

x := 2; w h i l e x > 0 d o x := x - 1

$x := 2;\ while\ x > 0\ do\ x := x - 1$

Martin Berger

9

Stan nie zmienia się, gdy weźmiemy pod uwagę, , aby zdecydować, czy do wykonywania jednej iteracji pętli, ale można to zmienić później , kiedy uruchomić ciała . Tak więc następnym razem, gdy rozważymy , może nastąpić zmiana . $\sigma$ $B$ $S$ $B$ $\sigma$

Andrej Bauer
źródło

Wyjaśnienie to, choć zasadniczo poprawne, nie odnosi się do tego, jakie stany są (mianowicie funkcja, która mówi nam o wartościach zmiennych) i co oznacza zmiana stanu (mianowicie, że zmienia się wartość co najmniej jednej zmiennej).

Hans Hüttel

Rzeczywiście, nie ma znaczenia, jakie są stany i jak są one wdrażane na potrzeby mojej odpowiedzi. Wyjaśnienie to obowiązuje. Co więcej, błędem jest twierdzenie, że „stany są naprawdę funkcjami”, ponieważ jest to tylko jeden sposób na ich matematyczne modelowanie. Istnieją inne możliwe modele. I nie pomylmy modeli matematycznych z działaniem sprzętu.

Andrej Bauer,

Pytanie dotyczy jednak konkretnej semantyki operacyjnej na małą skalę, dla której pojęcie stanu jest dobrze zdefiniowane.

Hans Hüttel

Nigdy nie powiedziałem, że nie. Mówię tylko, że twoja uwaga jest niepotrzebna, ponieważ moje wyjaśnienie nie zawiera wyraźnej wzmianki o tym, jak modelowany jest stan. Być może wykryłeś, że OP nie wiedział, że stan jest mapą od zmiennych do wartości. Dobrze dla ciebie, odpowiedź została zaakceptowana, a ja nie. Gratulacje. Dlaczego teraz narzucasz mi swój sposób odpowiedzi, nie rozumiem. Dlaczego dokładnie czujesz potrzebę, by moja odpowiedź była taka jak Twoja? Moja odpowiedź ma sens bez uwag, które uważasz za konieczne. Być może pewnego dnia ktoś przyjdzie, szukając mojej odpowiedzi.

Andrej Bauer,

Dlaczego stan pozostaje niezmieniony w niewielkiej semantyce operacyjnej pętli while?

Odpowiedzi: