Semantyka instrukcji, to funkcja \( I:{\cal V}\times {\cal P} arrow {\cal V} \)Rzeczywistość pokaże, że będziemy to nasze życzenie musieli lekko zmodyfikować, ale z grubsza nam na razie wystarczy. Cały problem polega teraz na tym, żeby precyzyjnie tę funkcję zdefiniować. Będziemy musieli zatem podać składnię instrukcji \( P \), a potem dla każdej instrukcji i każdego wartościowania \( V \) określić, do jakiego wartościowania \( V' \) wykonanie tej instrukcji prowadzi. Wprowadźmy następującą notację
\( I_V(P)=V' \) oznacza, że w stanie \( V \) wykonanie instrukcji \( P \) prowadzi do stanu \( V' \).
Zatem samo \( I_V \) będzie oznaczało funkcję ze zbioru \( {\cal P} \) w zbiór \( {\cal V} \). Funkcja ta związana z wartościowaniem \( V \) będzie mówiła, do czego doprowadzi nas wykonanie w tym stanie instrukcji \( P \). Podamy teraz składnię instrukcji naszych programów.
<instrukcja>. ::=<instrukcja pusta>|<instrukcja przypisania>|<instrukcja złożona>| <instrukcja warunkowa>|<instrukcja pętli>|<instrukcja pisania>|<instrukcja czytania>| <wywołanie procedury>
Po kolei będziemy teraz objaśniali składnię i semantykę poszczególnych typów instrukcji.
Składnia: <instrukcja pusta> ::= \( \varepsilon \). Semantyka: \( I_V(\varepsilon)=V \). Na dobry początek coś bardzo łatwego. Zażyczyliśmy sobie instrukcji pustej, która nie ma widzialnej postaci – jest pustym ciągiem znaków i nic nie robi: wykonana dla każdego wartościowania \( V \), pozostawia je niezmienionym. Jest to może mało ambitne zadanie, ale nie jest zabronione i w pewnych sytuacjach może być wygodne. Odłóżmy na później dyskusję dlaczego.
Składnia: <instrukcja przypisania> ::= <zmienna>:=<wyrażenie>. Zauważmy, że wszystkie instrukcje przypisania są postaci x:=E, gdzie x jest symbolem zmiennej, a E wyrażeniem, które umiemy już i zapisywać i interpretować. Semantyka: \( I_V({\tt x:=E})=V' \), gdzie. \( V'(z) = \begin{cases}V(z) & \textrm{\ jeśli } z \neq x \\ I_V(E) & \textrm{\ jeśli } z = x\end{cases} \) Czyli instrukcja przypisania x:=E nie zmienia wartości żadnej zmiennej poza \( x \), której to wyróżnionej zmiennej przypisuje wartość wyrażenia \( E \) przy wartościowaniu \( V \). Widzimy więc, że w wyrażeniu w szczególności może wystąpić ta sama zmienna \( x \), która znajduje się z lewej strony przypisania i jedyne, czego wymagamy, to żeby wartość tego wyrażenia była obliczona dla starego wartościowania.
Składnia: <instrukcja złożona> ::= begin <ciąg instrukcji> end
<ciąg instrukcji>::=\( \varepsilon \)|<instrukcja>;<ciag instrukcji>
Semantyka:
Zauważmy, że wszystkie instrukcje złożone są postaci begin \( \ P_1;\ldots;P_n\ \)end, gdzie \( P_1,\ldots P_n \) są instrukcjami.
\( I_V ({\tt begin }\ P_1; \ldots;P_n\ {\tt end}) = \begin{cases}V & \textrm{\ jeśli } n = 0 \\ I_V(P_1) & \textrm{\ jeśli } n = 1 \\ I_{I_V(P_1)} ({\tt begin}\ P_2; \ldots;P_n\ {\tt end}) & \textrm{\ jeśli } n > 1\end{cases} \)
Zatem jeśli między nawiasami begin a end nie ma żadnej instrukcji, to semantyka jest taka, jak instrukcji pustej; jeśli jest dokładnie jedna instrukcja, to semantyka jest dokładnie taka, jak tej jedynej instrukcji, a jeśli wewnątrz nawiasów występuje więcej niż jedna instrukcja, to po kolei wykonujemy je przechodząc od stanu \( V=V_0 \) kolejno przez stany \( V_1,\ldots,V_n \), tak że dla każdego \( 1\le i\le n \) zachodzi \( I_{V_{i-1}}(P_i)=V_i \). Wykonanie instrukcji złożonej polega więc na przejściu przez ciąg stanów pośrednich powstających przez wykonanie kolejnych instrukcji składowych. Z przyjętych założeń wynika, że jeśli którakolwiek z instrukcji składowych spowoduje błąd, to wartością całej instrukcji złożonej jest również błąd.
Do zdefiniowania instrukcji warunkowej będzie nam potrzebne rozróżnienie jej dwóch postaci: będziemy je nazywali instrukcją warunkową bez else'a oraz instrukcją warunkową z else.
Składnia:
<instrukcja warunkowa>::=<instrukcja warunkowa bez else>|<instrukcja warunkowa z else>
<instrukcja warunkowa bez else>::= if <wyrażenie logiczne> then <instrukcja>
<instrukcja warunkowa z else>::= if <wyrażenie logiczne> then <instrukcja, ale jeśli warunkowa to tylko z else> else <instrukcja>.
Rzecz jasna symbol <instrukcja, ale jeśli warunkowa to tylko z else> przechodzi na wszystkie instrukcje poza jedną: instrukcją warunkową bez else'a. Może zdziwić nieco ten łamaniec: na pierwszy rzut oka wydaje się niepotrzebną komplikacją wyłączenie w instrukcji z „else” jednego rodzaju instrukcji jako tej, która następuje po „then”. W rzeczywistości był to jeden z poważniejszych błędów koncepcyjnych w historii tworzenia języków programowania: tak właśnie myśleli twórcy znanego i bardzo popularnego w latach 60. języka programowania Algol 60 i przez parę lat programiści programowali za pomocą niejednoznacznych instrukcji. Problem ten stanie się widoczny po zdefiniowaniu semantyki.
Semantyka:
Zauważmy, że wszystkie instrukcje warunkowe są jednej z dwóch postaci: if \( \ B\ \) then \( \ P\ \) lub if \( \ B\ \) then \( \ P_1\ \) else \( \ P_2\ \), gdzie \( B \) jest wyrażeniem logicznym, \( P_1 \) jest dowolną instrukcją poza instrukcja warunkową bez else'a, a \( P_2 \) dowolną instrukcją. Dla pierwszego rodzaju instrukcji określamy semantykę następująco:
\( I_V({\tt if }\ B\ {\tt then }\ P) = \begin{cases}I_V(P) & \textrm{\ jeśli } I_V(B) = true \\ V & \textrm{\ jeśli } I_V(B) = false \end{cases} \)
Dla drugiego rodzaju instrukcji określamy semantykę następująco:
\( I_V({\tt if }\ B\ {\tt then }\ P_1\ {\tt else }\ P_2) = \begin{cases}I_V(P_1) & \textrm{\ jeśli } I_V(B) = true \\ I_V(P_2) & \textrm{\ jeśli } I_V(B) = false\end{cases} \)
Sprawdźmy teraz, że wyłączenie instrukcji warunkowej bez else'a było konieczne w drugim rodzaju instrukcji warunkowej. Rozważmy następującą instrukcję:
Przykład programu:
<b>if</b> x>0 <b>then</b> <b>if</b> y>0 <b>then</b> x:=1 <b>else</b> x:=0
Gdybyśmy dopuścili instrukcję warunkową bez else'a jako możliwą dla tego, co pojawia się po „then”, wówczas możliwy byłby dwojaki rozbiór gramatyczny tej instrukcji:
W pierwszym przypadku na przykład dla danych początkowych \( x=-1, y=-2 \) wartością zmiennej \( x \) po wykonaniu tej instrukcji byłoby \( -1 \) - nic by się nie zmieniło, gdyż warunek \( x>0 \) byłby niespełniony i w ogóle nie przeszlibyśmy do wykonania tego, co jest po „then”. W drugim przypadku wykonałaby się instrukcja po „else”, czyli x:=0, co spowodowałoby przypisanie zmiennej x wartości \( 0 \). Zatem, w zależności od widzimisię kompilatora, nasz program mógłby dawać dwie różne wartości. Tak określona semantyka nie byłaby więc funkcją.
W naszej gramatyce niejednoznaczności już nie ma. Jedynym możliwym odczytem rozważanej wyżej instrukcji jest pierwszy. Zapamiętajmy
Jeżeli mamy kaskadę if'ów, to „else” zamyka zawsze ostatnio otwarty „if”.
Proszę sprawdzić, że nie ma możliwości innego odczytu kaskady ifów, niż przez zamykanie else'ami najbardziej aktualnych warunków.
Często spotykamy się z sytuacją, w której pewien ciąg czynności będziemy chcieli wykonywać, aż zostanie spełniony pewien warunek. W takiej sytuacji stosujemy instrukcję pętli, która musi określić, co ma spowodować zakończenie pętli oraz co w każdym obrocie pętli powinno się wykonać. W zasadzie wystarczyłaby jedna postać instrukcji pętli, ale że jest to bardzo często stosowana instrukcja, dozwolimy aby stosować wygodne składniowo warianty.
Składnia:
<instrukcja pętli>::=<instrukcja while> | <instrukcja repeat> | <instrukcja for>
<instrukcja while> ::= while <wyrażenie logiczne> do <instrukcja>
<instrukcja repeat> ::= repeat <ciąg instrukcji> until <wyrażenie logiczne>
<instrukcja for> ::= for <zmienna> := <wyrażenie> to <wyrażenie> do <instrukcja> |
for <zmienna> := <wyrażenie> downto <wyrażenie> do <instrukcja>
Skupimy się na instrukcji while, a następnie pozostałe instrukcje zdefiniujemy korzystając z semantyki pętli while. Semantyka instrukcji while wymaga wprowadzenia dodatkowej kategorii semantycznej. Pętle while są postaci while \( B \) do \( P \). Intencją naszą jest wykonywanie instrukcji \( P \) tak długo, jak długo będzie spełniony warunek \( B \). Co jednak, gdy warunek \( B \) zawsze będzie spełniony? Zgodnie z naszym życzeniem program powinien działać bez końca. I tak właśnie chcielibyśmy, żeby było. Zatem mamy tu do czynienia z nową sytuacją: program ani nie kończy się błędem, ani czymkolwiek innym, co można by nazwać stanem końcowym. Po prostu {zapętla się}. Dla takiej sytuacji wprowadzamy kolejne rozszerzenie dziedziny semantycznej: już nie tylko wektor wartościowań lub błąd może być wynikiem wykonania programu, ale również uznajemy za poprawną wartość semantyczną zapętlenie, które będziemy oznaczali przez loop.
Zatem dodajemy jeszcze jedną wartość do możliwych wyników programu. Poza stanem programu (czyli wektorem wartościowań zmiennych) oraz błędem, mamy też {\em zapętlenie}. Powstaje pytanie, jak określić, czy – zgodnie z warunkiem definiującym semantykę pętli – program zapętli się, czy nie. W końcu chcielibyśmy wiedzieć, którą z wartości końcowych nasz program przyjmie: czy się zapętli, czy dojdzie do stanu końcowego. I tu niespodzianka! Nasza ciekawość nie może zostać zaspokojona, przynajmniej w automatyczny sposób. Nie ma bowiem procedury rozstrzygającej, czy dany program się zatrzyma dla konkretnych danych. Własność tę odkrył w latach 30-tych XX wieku Alan Turing. Turing udowodnił, że nie ma metody sprawdzenia, czy program zatrzyma się, czy nie.
Wkrótce dowiemy się, jak można w wielu przypadkach taki problem rozstrzygnąć. Nauczymy się dowodzenia tego, że program się zatrzyma, ale nie będzie to ogólna metoda, tylko ograniczona do na szczęście dość szerokiej klasy programów.
Semantyka:
Zauważmy, że instrukcja pętli ma postać: while \( \ B\ \) do \( \ P\ \), gdzie \( B \) jest wyrażeniem logicznym, a \( P \) jest dowolną instrukcją. Dla pętli while określamy semantykę następująco:
\( I_V({\tt while }\ B\ {\tt do }\ P) = \begin{cases}V & \textrm{\ jeśli } I_V(B) = false \\ I_{I_V(P)}(\tt while)\ B\ {\tt do }\ P) & \textrm{\ jeśli } I_V(B) = true \end{cases} \)
Widzimy więc, że gdy przy wartościowaniu \( V \) warunek \( B \) ma wartość false, wówczas nic się nie dzieje: pozostajemy przy wartościowaniu \( V \) i idziemy dalej, tak jak gdybyśmy wykonali instrukcję pustą. Jeśli natomiast warunek \( B \) ma wartość true, wówczas wykonujemy instrukcję P i wracamy do punktu wyjścia. Żeby ta definicja była formalnie poprawna, potrzebne jest jeszcze jedno ustalenie. Widać bowiem, że mamy do czynienia z dwiema mozliwościami. Albo po skończonej liczbie obrotów pętli warunek B stanie się fałszywy i wtedy przerywamy wykonanie pętli wychodząc z niego z otrzymanym wartościowaniem, albo warunek B nie stanie się fałszywy nigdy i wtedy właśnie mamy do czynienia z sytuacją zapętlenia się programu. Ustalmy więc, że gdy program się zapętla, to jego semantyką jest pętla - trzecia z możliwości (oprócz wartościowania i błędu). Zapętlenie się programu jest zaraźliwe: wystarczy, żeby choć jedna instrukcja pętli nie zakończyła działania, a wartością całego programu będzie pętla.
Podamy teraz parę przykładów pętli while.
l:=0; <b>while</b> b <> 0 <b>do</b> <b>begin</b> b:=b div 2; l:=l+1 <b> end</b>
Ten fragment programu działa różnie w zalezności od tego, czy b jest liczbą ujemną, czy nieujemną. Dla liczb dodatnich oblicza logarytm z b zaokrąglony w dół. Dla zera pozostawia wartość 0. dla liczb ujemnych otrzymujemy zapętlenie, gdyż -1 div 2 = -1 .
Zauważmy, że pętla może ani razu się nie wykonać, jeśli warunek dozoru będzie miał wartość false od razu na początku działania pętli. Często zdarzają się nam sytuacje, kiedy chcielibyśmy, aby pętla wykonała się co najmniej raz i żeby o tym, czy dalej ma się wykonywać, czy nie, decydować pod jej koniec. Taka sytuacja występuje na przykład wtedy, gdy żądamy od użytkownika podania jakiejś danej, na przykład hasła. Powinniśmy tak długo żądać od niego wprowadzenia danej, aż spełni ona pewien warunek (na przykład poprawności hasła lub przekroczenia limitu prób). Ponieważ taka sytuacja jest bardzo typowa, więc wprowadzimy konstrukcję, która umożliwia zrobienie tego prościej niż za pomocą pętli while.
Pętla repeat wygląda następująco:
<b>repeat</b>
P1;
P2;
...
Pn
<b>until</b> BJej semantyka jest równoważna następującemu fragmentowi
<b>begin</b> P1; P2; ... Pn <b>while</b> not B <b>do</b> <b>begin</b> P1; P2; ... Pn <b>end</b> {<b>while</b> not b} <b>end</b>
Widzimy więc, że zgodnie z tym, co napisaliśmy wcześniej, najpierw jednokrotnie wykonuje się ciąg instrukcji \( P1; \ldots;Pn \), a potem dopóki warunek \( B \) nie będzie spełniony, powtarzamy ten sam ciąg instrukcji. Warto zwrócić uwagę na to, że używając pętli while negujemy warunek z pętli repeat. Pętla while bowiem działa dopóki podany warunek dozoru jest spełniony, a pętla repeat kończy działanie w pierwszej chwili, w której warunek dozoru jest spełniony przy jego sprawdzaniu.
Kolejny rodzaj pętli, bardzo często stosowany, wiąże się najczęściej z przetwarzaniem kolejnych liczb całkowitych, na przykład przy przetwarzaniu tablic, kiedy nimi indeksujemy elementy. Użycie tego rodzaju pętli umożliwia kompilatorowi optymalizację kodu i przyspieszenie jego działania, ale wiąże się z pewnymi niebezpieczeństwami, o których zaraz opowiemy.
Najpierw przyjrzyjmy się postaci pętli. Może być ona dwojakiego rodzaju: for i:=E1 to E2 do P lub for i:=E1 downto E2 do P. W pierwszym przypadku semantyką tej pętli jest semantyka równoważnej jej postaci
i:=E1;
<b>while</b> i<=E2 <b>do</b>
<b>begin</b>
P;
i:=i+1
<b>end</b>Zaczynamy zatem od przypisania zmiennej sterującej i wartości E1, a następnie wykonujemy instrukcję P oraz zwiększamy i o 1 tak długo, aż przekroczymy wartość E2. W drugim przypadku robimy to samo, tylko w drugą stronę, zmniejszając wartości zmiennej i o 1. Zatem semantyką instrukcji for i:=E1 downto E2 do P jest semantyka następującego kodu
i:=E1;
<b>while</b> i>=E2 <b>do</b>
<b>begin</b>
P;
i:=i-1
<b>end</b>W rzeczywistości kompilatory często odbiegają nieco od tej semantyki i wprowadzają usprawnienia, które mogą dawać wyniki różniące się od siebie. Rzecz w tym, że gdy uruchamiamy pętlę for, to kompilator stara się z góry przewidzieć, ile obrotów pętla wykona. Oblicza więc wartości wyrażeń \( E1,E2 \) na początku działania pętli i z góry ustawia stosowny rejestr, który będzie odliczał liczbę wykonanych obrotów pętli, aż ta spadnie do zera. Podobnie będzie postępował z tablicami indeksowanymi zmienną sterującą. Normalnie, gdy odwołujemy się do i-tego elementu tablicy A, to kompilator ustala adres stosownej komórki w następujący sposób. Pobiera adres \( a \) początku tablicy z tabeli symboli, którą sam tworzy na etapie deklaracji, wylicza wartość wyrażenia indeksującego – w tym przypadku \( i \) - oraz dodaje do \( a \) wartość \( i-1 \) przemnożoną przez wielkość w bajtach pojedynczego elementu tablicy.
W przypadku pętli for, gdybyśmy chcieli odwoływać się w każdym kroku do i-tego elementu, to wystarczy wiedzieć, że w poprzednim obrocie pętli byliśmy w poprzednim elemencie, więc uzyskanie aktualnego adresu jest znacznie prostsze – wystarczy wziąć poprzedni adres i dodać do niego liczbę bajtów przypadającą na 1 element tablicy. Jeśli mamy nawet bardziej skomplikowane wyrażenie indeksujące pętli, np. zamiast \( i \) powiedzmy \( 3*i+2 \), to nadal różnica między poprzednim, a bieżącym adresem będzie stała i tę wartość można raz ustalić na początku pętli, a następnie kolejne adresy wyznaczać dodając ją do poprzednich. Stosowne wartości – ostatnio używanego adresu oraz skoku – zazwyczaj przechowywane są w rejestrach procesora i w związku z tym dostęp do nich jest znacznie szybszy.
Aby to wszystko się udało, nie powinno się zmieniać ani wartości zmiennej sterującej pętlą, ani ograniczenia wartości, czyli \( E2 \). Zrobienie jednej z tych dwóch rzeczy powoduje nieobliczalne skutki, więc pętle w stylu for i:=1 to n do begin i:=i+1; n:=n-1 end są przejawem niezrozumienia o co chodzi w pętli for. Na szczęście praktyka pokazuje, że tego typu konstrukcje nie mają żadnego zastosowania, więc po prostu pamiętajmy:
W pętlach for nie wolno zmieniać wartości zmiennej sterującej ani wartości końcowego ograniczenia pętli.
Ciekawe jest pytanie, jaka jest wartość zmiennej sterującej po wykonaniu pętli for. Przyjmijmy, że jest ona nieokreślona. W każdym razie nie powinno się niczego o niej zakładać. W niektórych bowiem kompilatorach zmienna ta pod koniec pętli przyjmuje wartość równą wartości \( E2, \), a w niektórych o jeden większą, jak to by wynikało z semantyki określonej za pomocą pętli while. W naszym narzędziu do uruchamiania programów zmienna sterująca różni się o 1 od wartości \( E2 \), ale nie należy z tego w żadnym wypadku korzystać.
Gdyby nasz program nie komunikował się w czasie działania ze światem zewnętrznym, musiałby wszystkie dane mieć wpisane przed uruchomieniem w kodzie. W rzeczywistości komputery wymieniają informację ze światem zewnętrznym i często w trakcie ich działania trzeba podawać pewne dane. Bardzo często jesteśmy w sytuacji, w której komputer żąda od nas podania imienia, nazwiska, wieku, dokonania jakichś wyborów. Co to znaczy, że wprowadzimy takie dane? Program musi je jakoś zapamiętać, czyli nadać pewnym zmiennym wartości przez nas podane. Do tego służy właśnie instrukcja czytania.
Mamy tu jednak zupełnie nową sytuację. Jak uwzględnić w semantyce programu to, co użytkownik poda jako dane wejściowe? Jest to o tyle trudne, że liczba możliwych reakcji użytkownika jest potencjalnie nieograniczona. W związku z tym musimy zmienić znowu nieco naszą dziedzinę semantyczną. Ciąg kolejno podawanych danych będziemy reprezentowali w liście zwanej wejściową. Zakładamy, że wszystko co użytkownik przygotuje, niezależnie od tego, czy zrobi to w momencie, gdy dane są potrzebne, czy zawczasu, zostaje dopisywane na końcu tej listy. Program natomiast pobiera wartości z początku listy – te, które były tam umieszczone jako pierwsze. Technikę, w której dane są podawane nieco wcześniej niż trzeba i wykorzystywane we właściwym momencie nazywamy buforowaniem, a część pamięci wykorzystywaną do przechowywania takich danych buforem.
Składnia:
<instrukcja czytania> ::= Read(<ciąg zmiennych>).
<ciąg zmiennych> ::= <zmienna> | <zmienna>,<ciag zmiennych>
Semantyka:
Zauważmy, że wszystkie instrukcje wejścia są postaci Read(x1,...,xm), gdzie x1,...,xm są zmiennymi.
Aby określić semantykę instrukcji czytania, przyjmijmy, że zawartość listy wejściowej jest równa \( L_{in}=(v_1,\ldots,v_n); n\ge m \). W tej sytuacji jako stan komputera przyjmujemy parę \( (V,L_{in}) \).
Mamy wtedy \( I_{(V,L_{in})}({\tt Read(x1,...,xm))}= (V',L'_{in}) \), gdzie
\( V'(z) = \begin{cases}V(z) & \textrm{\ jeśli } z \notin \{x1,\ldots,xm\} \\ v_k & \textrm{\ jeśli } z = x_k\end{cases} \)
oraz
\( L'_{in}=v_{m+1},\ldots,v_n. \)
W wyniku wykonania instrukcji czytania Read(x1,...,xm) lista wejściowa \( L_{in}=\{v_1,\ldots,v_m\} \) zostanie skrócona o \( m \) początkowych wartości, a wartości \( v_1,\ldots,v_m \) zostają przypisane zmiennym \( x1,\ldots, xm \). Dodajmy jeszcze, że jeśli lista wejściowa jest krótsza niż \( m \), to program zawiesza działanie i czeka aż zostanie uzupełniona o brakujące wartości.
W przypadku instrukcji czytania musieliśmy wziąć pod uwagę listę wejściową, aby określić semantykę. Podobnie teraz będziemy się musieli odnieść do listy wyjściowej, służącej jako medium komunikacyjne ze światem zewnętrznym. Standardową realizacją takiej listy są monitory ekranowe, ale równie dobrze mogą to być pliki oraz inne urządzenia wyjścia takie jak drukarka czy ploter. Zakładamy zatem istnienie listy wyjściowej, która na początku działania programu jest pusta i w miarę jego działania zapełnia się napisami wygenerowanymi przez program.
Składnia:
<instrukcja pisania> ::= Write(<ciąg wyrażeń>).
<ciąg wyrażeń> ::= <wyrażenie> | <wyrażenie>,<ciag wyrażeń>
Semantyka:
Zauważmy, że wszystkie instrukcje pisania są postaci Write(e1,...,em), gdzie e1,...,em są wyrażeniami.
Aby określić semantykę instrukcji pisania przyjmijmy, że zawartość listy wyjściowej jest równa \( L_{out}=(v_1,\ldots,v_n) \). W tej sytuacji jako stan komputera przyjmujemy trójkę \( (V,L_{in},L_{out}) \). Instrukcja pisania nie zmieni ani wartościowania zmiennych \( V \), ani listy wejściowej \( L_{in} \). Zmieni natomiast listę wyjściową, dopisując na jej końcu wartości wyrażeń.
Formalnie:
\( I_{(V,L_{in},L_{out})}({\tt Write(e1,...,em))}= (V',L'_{in},L'_{out}) \),
gdzie
\( V'=V \)
\( L'_{in}=L_{in} \)
\( L'_{out}=v_1, \ldots, v_n, I_V (e1) , \ldots , I_V(em) \)
W wyniku wykonania instrukcji pisania Write(e1,...,em) lista wyjściowa \( L_{out}=\{v_1,\ldots,v_n\} \) zostanie wydłużona o \( m \) wartości wyrażeń wyliczonych przy wartościowaniu \( V \). Ani wartościowanie \( V \), ani lista wejściowa \( L_{in} \) nie ulegają zmianie przy wykonywaniu instrukcji pisania.
Wykonywaniu procedur poświęcony będzie osobny wykład. Przyjmijmy na razie, że gdy wywołujemy procedurę, wyliczamy wartości parametrów dla aktualnego wartościowania, a następnie wykonujemy kod procedury, używając wyliczonych wartości jako początkowych w naszych obliczeniach.