Semantyka i weryfikacja programów/Ćwiczenia 1

From Studia Informatyczne

Zawartość

Tematem tych zajęć jest semantyka operacyjna wyrażeń (małe kroki).


Semantyka operacyjna wyrażeń

Ćwiczenie 1

Rozważmy bardzo prosty język wyrażeń, którego składnia opisana jest następującą gramatyką:

n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots

x \, ::= \,\, \ldots \, (identyfikatory) \, \ldots

e \,  ::=  \,\,           n   \,\,|\,\,         x   \,\,|\,\,         e_1 + e_2   \,\,|\,\,         \mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3

Wynikiem wyrażenienia warunkowego \mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3 jest wartość wyrażenia e_2, o ile wyrażenie e_1 oblicza się do wartości różnej od zera; w przeciwnym przypadku wynikiem jest wartość wyrażenia e_3.

Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.


Rozwiązanie

Zacznijmy od ustalenia notacji i dziedzin syntaktycznych.

Niech \mathbf{Num} oznacza zbiór stałych liczbowych, n \in \mathbf{Num} = \{ 0, 1, \ldots \}. Podobnie, niech \mathbf{Var} oznacza zbiór identyfikatorów, które mogą być nazwami zmiennych; x \in \mathbf{Var}. Wreszcie, niech \mathbf{Exp} oznacza zbiór wyrażeń; e \in \mathbf{Exp}. Dla ułatwienia zapisywania reguł zakładamy, że stałe liczbowe są wyrażeniami, czyli \mathbf{Num} \subseteq \mathbf{Exp}.

Będziemy potrzebować zbioru "stanów", opisujących wartości przypisane zmiennym.

Najprostszym rozwiązaniem jest przyjąć, że stan to funkcja z \mathbf{Var} do \mathbf{Num}. Oznaczmy przez \mathbf{State} zbiór wszystkich takich funkcji; stany oznaczać będziemy przez s, s_1, s', \ldots \in \mathbf{State}.

W naszej semantyce będziemy potrzebowac tranzycji dwóch postaci.

Po pierwsze, tranzycje postaci

e, s \,\Longrightarrow\, e', s

oznaczające mały krok w trakcie obliczania wyrażenia e w stanie s, w wyniku którego e wyewoluowało do e'.

Stan nie ulega zmianie podczas obliczania wyrażenia (nie ma tzw. efektów ubocznych), więc to samo s figuruje po lewej i prawej stronie strzałki.

Po drugie, tranzycje postaci

e, s \,\Longrightarrow\, n

będą oznaczaczać, że wyrażenie e jest już policzone, a jego wartością jest n.

Zatem przyjmijmy, że zbiór konfiguracji to

( \mathbf{Exp} \times \mathbf{State} ) \, \cup \, \mathbf{Num}

a konfiguracje końcowe to \mathbf{Num}.

Uwaga

Tak naprawdę, druga postać tranzycji nie jest niezbędna, gdyż moglibyśmy umówić się, że konfiguracje końcowe to \mathbf{Num} \times \mathbf{State}.

Najprostsze są tranzycje prowadzące do konfiguracji końcowej:

n, s \,\Longrightarrow\, n

Symbol n po lewej stronie to wyrażenie składające się ze stałej liczbowej, podczas gdy n po prawej stronie reprezentuje liczbę będącą wartością wyrażenia.

Zmienna oblicza się do swojej wartości w bieżącym stanie:

x, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } s(x) = n.

Teraz zajmiemy się dodawaniem e_1 + e_2. Ponieważ semantyka jest w stylu małych kroków, musimy zdecydować się, czy najpierw obliczyć pierwszy (lewy) składnik e_1, czy drugi?

Jeśli wybierzemy lewy (strategia "lewostronna"), otrzymamy regułę:

e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s  \quad \mbox{ o ile } \quad e_1, s \,\Longrightarrow\, e'_1, s.

Reguły tej postaci będziemy zapisywać tak:

\frac{e_1, s \,\Longrightarrow\, e'_1, s}      {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s}

Czyli mały krok w e_1 stanowi też mały krok w e_1 + e_2.

Po zakończeniu obliczania e_1 przechodzimy do e_2:

\frac{e_2, s \,\Longrightarrow\, e'_2, s} {n + e_2, s \,\Longrightarrow\, n + e'_2, s}.

A na końcu dodajemy:

n_1 + n_2, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } n = n_1 + n_2.

Zwróćmy tutaj uwagę na pewną subtelność, dotyczącą dwóch wystąpień symbolu +: pierwsze wystąpienie oznacza jedną z konstrukcji składniowych języka, a drugie oznacza operację dodawania w zbiorze \mathbf{Num}.

Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest składnią abstrakcyjną, więc zamiast e_1 + e_2 moglibyśmy równie dobrze pisać np. {\mathrm{add}}(e_1, e_2), a wtedy reguła wyglądałaby tak:

\mathrm{add}(n_1, n_2), s \,\Longrightarrow\, n, s \quad \mbox{ o ile } n = n_1 + n_2.

Inną możliwą strategią obliczania e_1 + e_2 jest strategia "prawostronna", którą otrzymujemy zastępując pierwsze dwie z trzech powyższych reguł przez:

\frac{e_2, s \,\Longrightarrow\, e'_2, s}      {e_1 + e_2, s \,\Longrightarrow\, e_1 + e'_2} \quad \quad \frac{e_1, s \,\Longrightarrow\, e'_1, s}      {e_1 + n, s \,\Longrightarrow\, e'_1 + n, s}.

Ponadto, jeśli przyjmiemy regułę pierwszą (dla e_1), trzecią i czwartą (dla e_2), otrzymamy strategię "równoległą", polegającą na obliczaniu jednocześnie e_1 i e_2:

\frac{e_1, s \,\Longrightarrow\, e'_1, s}      {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s} \quad \quad \frac{e_2, s \,\Longrightarrow\, e'_2, s}      {e_1 + e_2, s \,\Longrightarrow\, e_1 + e'_2} \quad \quad n_1 + n_2, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } n = n_1 + n_2.

Bardziej precyzyjnie mówiąc, małe kroki obliczające obydwa podwyrażenia przeplatają się, i to w dowolny sposób.

Ta dowolność prowadzi do niedeterminizmu, czyli do sytuacji, gdy kolejna (następna) konfiguracja nie jest wyznaczona jednoznacznie. Jest tak, gdyż możemy mieć do wyboru dwie różne tranzycje

e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s  \quad \quad \quad e_1 + e_2, s \,\Longrightarrow\, e_1 + e'_2, s.

Zauważmy natomiast, że kolejność przeplatania się małych kroków obliczających e_1 i e_2 nie wpływa w tym przypadku na końcową wartość całego wyrażenia.

Na koniec reguły dla wyrażenia warunkowego.

\frac{e_1, s \,\Longrightarrow\, e'_1, s}      {\mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\Longrightarrow\, \mathbf{if}\, e'_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s}

\mathbf{if}\, n \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\Longrightarrow\, e_2, s \quad \mbox{ o ile } n \neq 0

\mathbf{if}\, n \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\Longrightarrow\, e_3, s \quad \mbox{ o ile } n = 0


Ćwiczenie 2

Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję

e \,  ::=  \,\,           \ldots   \,\,|\,\,         \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2

Wyrażenie \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 zawiera w sobie deklarację x = e_1, która stanowi mechanizm wiązania identyfikatorów w naszym języku. Deklaracja x = e_1 wprowadza nową zmienną x oraz przypisuje jej wartość. Wartość wyrażenia \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 obliczamy następująco: najpierw oblicza się wartość e_1, podstawia ją za zmienną x, a następnie oblicza wyrażenie e_2. Zakresem zmiennej x jest wyrażenie e_2, czyli wewnątrz e_2 można odwoływać się (wielokrotnie) do zmiennej x; Ogólniej, odwołania do zmiennej w wyrażeniu odnoszą się do "najbliższej" (najbardziej zagnieżdzonej) deklaracji tej zmiennej. Taki mechanizm wiązania identyfikatorów nazywamy wiązaniem statycznym. Przyjmujemy zwykłe (statyczne) reguły przesłaniania zmiennych, np. jeśli w e_2 występuje podwyrażenie \mathbf{let}\, x = e \,\mathbf{in}\, e', to deklaracja x = e "przesłania" deklarację x = e_1 w wyrażeniu e'.

Zakładamy, że na początku wartości wszystkich zmiennych są nieokreślone, czyli zmienne są niezainicjowane, a odwołanie do niezainicjowanej zmiennej jest uważane za niepoprawne.


Przykład

\mathbf{let}\, x = 0 \,\mathbf{in}\, \mathbf{let}\, y = 7 \,\mathbf{in}\, \mathbf{let}\, x = y+3 \,\mathbf{in}\, x+x+y  \quad \quad \mapsto \quad \quad \mbox{wynik} = 24

\mathbf{let}\, y = 5 \,\mathbf{in}\, \mathbf{let}\, x = (\, \mathbf{let}\, y = 3 \,\mathbf{in}\, y+y \,) \,\mathbf{in}\, x+y \quad \quad \mapsto \quad \quad \mbox{wynik} = 11

\mathbf{let}\, z = 5 \,\mathbf{in}\, x+z \quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej zmiennej}\, x

\mathbf{let}\, x = 1 \,\mathbf{in}\, \mathbf{let}\, x = x+x \,\mathbf{in}\, x+x \quad \quad \mapsto \quad \quad \mbox{wynik} = 4


Rozwiązanie

Podobnie jak poprzednio, stan powinien opisywać wartości przypisane zmiennym.

Tym razem jednak uwzględnimy niezainicjowane zmienne, czyli zmienne bez żadnej wartości. Przyjmijmy zatem, że stan to skończona funkcja częściowa z \mathbf{Var} do \mathbf{Num}. Oznaczmy symbolem \mathbf{State} zbiór wszystkich takich funkcji: \mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num}. Naturalnym stanem początkowym jest stan "pusty", tzn. pusta funkcja częściowa, który będziemy oznaczać symbolem \emptyset. Wartość wyrażenia e w stanie początkowym wynosi n, o ile zachodzi:

e, \emptyset \,\Longrightarrow^{*}\, n.

Będziemy potrzebowac tranzycji dwóch postaci, podobnie jak poprzednio, ale pierwsza postać będzie nieco ogólniejsza:

e, s \,\Longrightarrow\, e', s'.

Tranzycja ta oznacza mały krok w trakcie obliczania wyrażenia e w stanie s, w wyniku którego e wyewoluowało do e', a nowym stanem jest s'.

Stan może się teraz zmienić na skutek deklaracji zmiennych.

Spróbujmy rozszerzyć semantykę z poprzedniego zadania.

Ponieważ stan jest funkcją częściową, musimy zmienić niektóre reguły, np.

x, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } s(x) \mbox{ jest określone i } s(x) = n

Następnie dodajemy reguły dla wyrażenia \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2.

Gdy e_1 jest już obliczone, wystarczy reguła:

\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2, s[x \mapsto n].

Notacja s[x \mapsto n] oznacza stan s, który zmodyfikowano przypisując zmiennej x wartość n, niezależnie od tego, czy s(x) było określone, czy nie, i pozostawiając niezmienione wartości dla pozostałych zmiennych.

Formalnie

s[x \mapsto n](y) =  \begin{cases} n    & y = x \\ s(y) & y \neq x \end{cases}

W szczególności dla y \neq x, s[x \mapsto n](y) jest określone wtedy i tylko wtedy, gdy s(y) jest określone.

Natomiast aby obliczyc e_1, potrzebujemy reguły:

\frac{e_1, s \,\Longrightarrow\, e'_1, s'} {\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\Longrightarrow\, \mathbf{let}\, x = e'_1 \,\mathbf{in}\, e_2, s'}

Zwróćmy uwagę, że stan s' może być różny od s, np. dlatego, że wewnątrz e_1 znajduje się podwyrażenie \mathbf{let}\, y = \ldots.

Pytanie: czy taka semantyka jest poprawna?

Niestety nie, gdyż nie uwzględniamy ograniczonego zasięgu zmiennej.

Rzućmy okiem na przykład:

\mathbf{let}\, x = (\mathbf{let}\, z = 4 \,\mathbf{in}\, z+z+z) \,\mathbf{in}\, z

Według naszych intencji to wyrażenie nie ma wartości, gdyż ostatnie odwołanie do z jest błędne.

Natomiast według powyższych reguł mamy

\mathbf{let}\, x = (\mathbf{let}\, z = 4 \,\mathbf{in}\, z+z+z) \,\mathbf{in}\, z, \emptyset \,\Longrightarrow\, \mathbf{let}\, x = z+z+z \,\mathbf{in}\, z, \emptyset[z \mapsto 4] \,\Longrightarrow\, \quad \ldots \quad \,\Longrightarrow\, \mathbf{let}\, x = 12 \,\mathbf{in}\, z, \emptyset[z \mapsto 4] \,\Longrightarrow\,  12, \emptyset[z \mapsto 4] \,\Longrightarrow\,  12 !

Nasz błąd polega na tym, że po zakończeniu obliczania podwyrażenia \mathbf{let}\, z = 4 \,\mathbf{in}\, z+z+z "zapominamy" przywrócić zmiennej z poprzednią wartość (a właściwie brak wartości w przykładzie powyżej).

Przedyskutujmy kilka wariantów.


Wariant 1

Wygodne i eleganckie rozwiązanie tego problemu jest możliwe, jeśli rozszerzymy składnię naszego języka.

Intuicyjnie, reguła

\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2, s[x \mapsto n].

powinna zostać zastąpiona przez

\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, \mbox{"przywróć wartość zmiennej x"}, s[x \mapsto n].

czyli potrzebujemy konstrukcji składniowej, która polega na obliczeniu wyrażenia e_2, a następnie na przypisaniu zmiennej x danej wartości.

Rozszerzmy zatem składnię następujaco:

e \,  ::=  \,\,           \ldots   \,\,|\,\,         e \,\mathbf{then}\, x := n.

Wyrażenie e \,\mathbf{then}\, x:= n jest w pewnym sensie dualne do \mathbf{let}\, x = n \,\mathbf{in}\, e, gdyż jedyna (choć niewątpliwie istotna) różnica między nimi to kolejność obliczenia e i przypisania wartości na zmienną x.

Oto nowa reguła

\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, x := n', s[x \mapsto n] \quad \mbox{ o ile } s(x) = n'.

Pewna trudność pojawia się w sytuacji, gdy s(x) jest nieokreślone, czyli gdy zmienna x jest niezainicjowana -- reguła powyższa nie obejmuje wogóle takiej sytuacji.

Najprostszym sposobem rozwiązania tej trudności jest rozszerzenie konstrukcji e \,\mathbf{then}\, x := n:

e \,  ::=  \,\,           \ldots   \,\,|\,\,         e \,\mathbf{then}\, x := n  \,\,|\,\,         e \,\mathbf{then}\, x := \bot

gdzie symbol \bot oznacza brak wartości.

Dodajemy również regułę:

\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, x := \bot, s[x \mapsto n] \quad \mbox{ o ile } s(x) \, \mbox{ jest nieokreślone}.

Rozwiązanie to jest odrobinę nieeleganckie, gdyż prawie identyczne reguły musimy napisać dwukrotnie.

Widać to np. w poniższych regułach, "scalających" semantykę dla e \,\mathbf{then}\, x := n z semantyką pozostałych wyrażeń:

\frac{e, s \,\Longrightarrow\, e', s'} {e \,\mathbf{then}\, x := n, s \,\Longrightarrow\, e' \,\mathbf{then}\, x:= n, s'}

n' \,\mathbf{then}\, x := n, s \,\Longrightarrow\, n', s[x \mapsto n]

n' \,\mathbf{then}\, x := \bot, s \,\Longrightarrow\, n', s' \quad \mbox{ o ile } s(x)  \mbox{ jest określone i } s' = s \setminus \{ (x, s(x)) \}


Wariant 2

Zanim przejdziemy do kolejnego wariantu, zastanówmy się, czy istnieje inny sposób rozwiązania trudności związanej z n = \bot, który pozwalałby uniknąć wprowadzania dodatkowej konstrukcji

e \,\mathbf{then}\, x := \bot. Pomysł może polegać na rozszerzeniu zbioru \mathbf{Num} o dodatkowy element \bot:

n \, ::= \,\, \bot \,\,|\,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots

Wtedy nie musimy pisać dwóch bardzo podobnych wariantów reguł.

Dodatkowo, w tym rozwiązaniu warto poczynić umowę, że s(x) = \bot reprezentuje brak wartości zmiennej x. Wtedy stany są funkcjami całkowitymi z \mathbf{Var} w \mathbf{Num}, przyjmującymi wartość różną od \bot tylko dla skończenie wielu elementów. Pewnym mankamentem jest to, że teraz n = \bot może pojawiać się w wyrażeniach podobnie jak stałe. Tym niemniej nie musimy adaptować reguł dla stałych tak, aby radziły one sobie z n = \bot, ponieważ wyrażenia zawierające \bot możemy również uważać za roszerzenie składni.

Jeśli jednak dopuścimy symbol \bot w wyrażeniach, to możemy elegancko wybrnąć z sytuacji, rozszerzając operacje arytmetyczne na zbiór \mathbf{Num} \cup \{ \bot \} tak, aby zachowywały one nieokreśloność:

n + \bot = \bot + n = \bot.

Trzeba jednak w takim razie zadbać o to, aby wyrażenie \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 obliczało się normalnie tylko wtedy, gdy wartość wyrażenia e_1 jest różna od \bot.

,
Wariant 3

Zrewidujmy teraz podstawowe założenia, które dotychczas poczyniliśmy.

Jednym z nich było przyjęcie ogólnej postaci tranzycji:

e, s \,\Longrightarrow\, e', s'

pozwalającej na zmianę stanu podczas obliczania wyrażenia.

Czy faktycznie był to dobry pomysł? Czy moglibyśmy poradzić sobie przy pomocy tranzycji postaci

e, s \,\Longrightarrow\, e', s ?

Spróbujmy! Oto nowa wersja jednej z reguł dla \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, dotycząca kroku wewnątrz e_1:

\frac{e_1, s \,\Longrightarrow\, e'_1, s} {\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\Longrightarrow\, \mathbf{let}\, x = e'_1 \,\mathbf{in}\, e_2, s}

Dotychczas nie ma problemu: podwyrażenie e_1 jest prawidłowo obliczane w stanie s. Trudność pojawi się, gdy

zakończymy obliczanie e_1 i przejdziemy do e_2. Oto możliwa reguła:

\frac{e, s[x \mapsto n] \,\Longrightarrow\, e', s[x \mapsto n] }      {\mathbf{let}\, x = n \,\mathbf{in}\, e, s \,\Longrightarrow\, \mathbf{let}\, x = n \,\mathbf{in}\, e', s}.

Okazuje się, że wszystko jest w porządku. Wyrażenie e obliczamy w prawidłowym stanie, tzn. z wartością n przypisaną zmiennej x.

Mały krok w e daje przyczynek do małego kroku w całym wyrażeniu, a przy tym stan pozostaje niezmieniony. Przy tym wogóle nie potrzebujemy przywracać poprzedniej wartości zmiennej x, ponieważ x zyskuje nową wartość "tylko" na potrzeby obliczania podwyrażenia e! Można na to również spojrzeć inaczej: informacja o nowej wartości n dla zmiennej x nie jest jawnie dodawana do stanu s, ale jest przechowywana w składni wyrażenia \mathbf{let}\, x = n \,\mathbf{in}\, \ldots jako deklaracja x = n. Na końcu musimy oczywiście pozbyć się tej deklaracji za pomocą następującej tranzycji:

\mathbf{let}\, x = n \,\mathbf{in}\, n', s \,\Longrightarrow\, n', s

Podsumujmy. Okazuje się, że rozwiązanie nie było wcale łatwe, nawet dla tak prościutkiego języka. W przyszłości przekonamy się, że łatwiej jest poradzić sobie z zagadnieniem wiązania identyfikatorów w semantyce naturalnej (duże kroki).

W wariancie 1 i 2 wprowadziliśmy do języka dodatkowe elementy, tak by łatwiej było pisać reguły. W przyszłości będziemy czasem stosować takie podejście. Niekiedy jednak rozszerzanie języka będzie zabronione.

Zadania domowe

Ćwiczenie 1

Zapisz wariant 2 semantyki z poprzedniego zadania.


Ćwiczenie 2

Dotychczas wystąpienie błędu podczas obliczania wyrażenia, np. odwołanie do niezainicjowanej zmiennej, powodowało, że wyrażenie nie posiadało wartości (nie było ciągu tranzycji prowadzących do konfiguracji końcowej). Zmodyfikuj którąś z semantyk z poprzednich zadań tak, aby błąd był komunikowany jako jedna z konfiguracji końcowych. To znaczy: jeśli obliczenie wyrażenia e w stanie s jest niemożliwe bo wystąpił błąd, to

e, s \,\Longrightarrow^{*}\, \mathtt{Blad}.


Ćwiczenie 3

Rozważ rozszerzenie języka wyrażeń o wyrażenia boolowskie:

n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots

x \, ::= \,\, \ldots \, (identyfikatory) \, \ldots

b \, ::= \,\,          \mathbf{true}   \,\,|\,\,         \mathbf{false}  \,\,|\,\,         e_1 \leq e_2  \,\,|\,\,         \neg b  \,\,|\,\,         b_1  \land  b_2

e \,  ::=  \,\,           n   \,\,|\,\,         x   \,\,|\,\,         e_1 + e_2   \,\,|\,\,         \mathbf{if}\, b \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3  \,\,|\,\,         \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2

Zaproponuj semantykę małych kroków dla tego języka. Rozważ różne strategie obliczania wyrażeń boolowskich, oraz podejście leniwe. Na przykład w strategii lewostronnej dla b_1 \land b_2, gdy b_1 zostało obliczone do \mathbf{false}, w podejściu leniwym nie ma wogóle potrzeby obliczania b_2.