PROGRAM STATIKUS FOGALMA DINAMIKUSAN VÁLTOZÓ ÁLLAPOTTÉRBEN1 Az ELTE IK programozó informatikus képzésében egy statikus szemléletű, matematikai relációk fogalmára épülő modell keretében tanítjuk a programozást. [3][6] Ez a modell már majdnem harminc éve megszületett, folyamatosan csiszolódott, de a legfontosabb alapfogalmai nem változtak meg. Most néhány alapfogalmát módosítom, de úgy, hogy érvényben maradjanak a modell keretében bizonyított eredmények, ugyanakkor két ponton rugalmasabbá váljon. Könnyebb legyen az úgynevezett kiterjesztési problémákat (beszélhetünk-e megoldásról, ha a feladat és a program állapotterei nem azonosak, hanem egyik a másiknak altere) megválaszolni és lehessen az absztrakt programok szintjén alprogramokról illetve alprogramok hívásáról beszélni (és ezzel együtt rekurzívan hívható alprogramokat is megadni).
1. Alapfogalmak Induljunk ki abból a megállapításából, amely szerint a programozás egy olyan tevékenység, amikor egy feladat megoldására programot készítünk. Ennek értelmében a programozás három alapfogalomra épül: a feladat, a program és a megoldás fogalmaira. Mi az a feladat, mi az a program, mit jelent az, hogy egy program megold egy feladatot? Erre adok itt választ. A válaszokban az állapottér és a program fogalmai lesznek újak a programozási modell korábbi definícióihoz képest.
2. Az adatok típusa Az adattípus fogalma nem változott a modell eredeti változatához képest. Definíció. Egy adat típusát az adat által felvehető lehetséges értékek halmaza, az úgynevezett típusérték-halmaz, és az ezen értelmezett műveletek, az úgynevezett típusműveletek együttesen határozzák meg, más szóval specifikálják2.
3. Állapottér Tekintsünk néhány adatot az adattípusaikkal. Vezessünk be olyan páronként különböző neveket, amelyekkel az adatokat egyértelmű módon megcímkézhetjük. Ha minden adatnak vesszük egy-egy lehetséges értékét, és minden értéket a saját adata címkéjével megjelöljük, akkor ezt az érték-együttest állapotnak nevezzük. Az állapottér az összes lehetséges állapot halmaza.
1
2
Készült a TÁMOP 4.2.1./B-09/1/KMR-2010-0003 számon regisztrált pályázat keretében.
A típus korszerű definíciója ennél jóval árnyaltabb, de egyelőre ez a szűkített változat is elegendő lesz az alapfogalmak bevezetésénél.
Definíció. Legyenek az A1, ... , An (nℕ+) típusérték-halmazok. Rendeljünk hozzájuk egyedi (páronként különböző) c1, ... , cn címkéket. Ekkor a { {c1:a1 , ... , cn:an} aiAi (i=1,...,n) } halmazt az A1, ... , An típusérték-halmazokból képzett állapottérnek nevezzük, amit a továbbiakban a (c1:A1 , ... , cn:An) szimbólummal jelölünk. Az állapottér elemei (amelyek maguk is halmazok: címkézett értékek halmazai) az állapotok. A (c1:A1, ... , cn:An) állapottérnek a ci-vel címkézett Ai halmazát (i{1...n}) az állapottér komponensének hívjuk. A {c1:a1, ... , cn:an} állapot ci-vel (i{1...n}) címkézett komponensén az ai értéket értjük. Definíció. Az A = (c1:A1, ... , cn:An) állapottér bármely ci (i=1, ... ,n) címkéje azonosít egy olyan ci:AAi (vetítő vagy projekciós) függvényt, amely minden aA állapothoz annak ci címkéjű komponensét rendeli, azaz ha a = {c1:a1, ... , cn:an}, akkor ci(a)=ai. Ezt a függvényt az állapottér változójának nevezzük. A fenti definíció biztosítja, hogy mind az állapottér, mind egy állapot komponenseire egyértelmű módon lehessen hivatkozni, ugyanakkor nem jelöl ki feleslegesen sorrendet a komponensek között, mint azt egy direktszorzattal megadott állapottér tenné. A direktszorzattal megadott terekhez hasonlóan itt is be lehet vezetni az altér fogalmát. Definíció. Tekintsük az A=(c1:A1 , ... , cn:An) állapotteret és az :{1..m}{1..n} (n,mℕ+, m≤n) indexsorozatot. Ekkor a B=(c(1):A(1) , ... , c(m):A(m)) állapotteret az A egy alterének nevezzük és ezt B≤A-val jelöljük. A definícióból adódik, hogy ha B=(d1:B1 , ... , dm:Bm) állapottér altere az A=(c1:A1 , ... , cn:An) állapottérnek, akkor a B-beli címke-komponens párok mind előfordulnak A-ban, azaz {d1:B1 , ... , dm:Bm }{c1:A1 , ... , cn:An }. Definition. Let A=(c1:A1 , ... , cn:An) and B= (ci1:Ai1 , ... , cim:Aim) (n,mℕ+, m≤n, {i1, … , im}{1, … , n}) be state spaces and B≤A. A prB:AB leképezést az A állapottér B-re vett vetítésének (projekciójának) nevezzük, ha minden A-beli {c1:a1 , ... , cn:an} állapotra a prB({c1:a1 , ... , cn:an})={c(1):a(1) , ... , c(m):a(m) }. A vetítés segítségével nemcsak egy állapot képezhető át egy altérbe, hanem állapotpárok, állapotsorozatok és állapothalmazok is, amennyiben azok vetítését állapotonként végezzük el.
4. Feladat fogalma A feladat fogalma nem változott. Definíció. Legyen az A egy állapottér. Ekkor az FAA relációt az A feletti feladatnak nevezzük. (Ez a definíció nem változott.)
5. Program fogalma A program az általa befutható összes lehetséges végrehajtás együttese. Rendelkezik egy alapállapottérrel, amelyiknek bármelyik állapotából el tud indulni, és ahhoz olyan végrehajtási
sorozatokat rendel, amelyik első állapota a kiinduló állapot. Ugyanahhoz a kiinduló állapothoz akár több végrehajtási sorozat is tartozhat. Egy végrehajtási sorozat további állapotai az alap-állapottér komponensein kívül segéd komponenseket is tartalmazhatnak, de ezek a véges hosszú végrehajtások esetén legkésőbb az utolsó lépésében megszűnnek, így a véges végrehajtások az alap-állapottérben terminálnak. A program formális definíciója előtt vezessünk be néhány jelölést! Jelölje H** a H halmaz elemeiből képzett összes (véges és végtelen hosszú) sorozatot tartalmazó halmazt. Jelölje a H a végtelen hosszú sorozatok halmazát, a H* pedig – korábbi jelölésünkkel összhangban – a H halmaz elemeiből képzett véges hosszú sorozatokat tartalmazza. Nyilvánvaló, hogy H** = H*H. Egy H** sorozat hosszát a || szimbólummal írjuk le, amely értéke végtelen hosszú sorozat esetén . Adjuk meg ezek utána program formális definícióját. Definíció., Legyen A egy állapottér, és a A az összes olyan állapot halmaza, amelyek azon állapotterekhez tartoznak, amelyeknek altere az A, azaz A
B . Ekkor az SA A
relációt az A
A B
állapottér feletti programnak hívjuk (A a program alap-állapottere), ha 1.
S=A
és minden S A -ra: ||A.
2. minden aA-ra és minden S(a)-ra: ||1 és 1=a. Új, a korábbi modellben nem szereplő fogalom az alap-állapottér. A program csak az alapváltozóin keresztül tud a környezetével kapcsolatot teremteni. Egy alapváltozónak tudunk „kívülről” kezdőértéket adni, és egy alapváltozóból tudjuk a terminálás után az eredményt lekérdezni. A program fogalmának új eleme az is, hogy egy végrehajtás során új komponensek jöjjenek létre, és szűnjenek meg az állapottérben. Ugyanakkor feltesszük, hogy termináláskor a végállapotban már csak a kezdetben létező komponensek (az alap-állapottér komponensei) szerepelhetnek. A program egy végrehajtása során dinamikusan változik az állapottér, de az éppen aktuális állapottérnek mindig komponensei lesznek az alap-állapottér komponensei. Egy program működése nyilvánvalóan nem változik meg attól, ha az alap-állapotterének változóit átnevezzük. Arra kell csak ügyelni, hogy az új változónevek továbbra is komponensenként egyediek legyenek. Definíció. Legyen S egy A=(c1:A1 , ... , cn:An) állapottér feletti program, és a B=(d1:B1 , ... , dm:Bm) (n≤m) egy állapottér úgy, hogy van olyan :{1..n}{1..m} injekció, hogy Ai = B(i) (i{1...n}). Az S program változó-átnevezésének nevezzük azt a B feletti programot, amelynek végrehajtási sorozatait S program végrehajtási sorozatai alkotják azzal a módosítással, hogy azok állapotaiban mindenhol a ci változónevet d(i) változónévre cseréljük, és ha di segédváltozóként szerepelt az S programban, akkor a segédváltozó nevét is egyedi névre cseréljük le.
Egy program működése attól sem változik meg, ha a változóinak státuszán módosítunk: néhányat alapváltozóból segédváltozóvá, néhányat segédváltozóból alapváltozóvá minősítünk át. Egy alapváltozó ugyanis könnyedén átminősíthető segédváltozóvá úgy, hogy az csak a program elindulásakor jöjjön létre, és a program befejeződésekor megszűnjön. Egy segédváltozóból is lehet alapváltozó, ha már eleve létezőnek tekintjük, ezért nem kell sem létrehozni sem megszüntetni, élettartama mindegyik végrehajtás teljes hosszára kiterjed. Definíció. Legyen S egy A=(v1:A1 , ... , vn:An) állapottér feletti program és az A komponenseitől különböző v:T komponens. (A v lehet az S működése során megjelenő segédváltozó, de lehet azoktól teljesen független új változó is.) Az S program alap-állapotterének kibővítésén azt a programot értjük (jelöljük ezt S’-vel), amelynek alap-állapottere a C=(v1:A1 , ... , vn:An , v:T), és minden cC-re S’(c) = { C
S(prA(c)) : ||=|| és 1=prA(1) and i[2..||]: (i-nek nincs v komponense i = (i, v:v(i-1)) (i-nek van v komponense) i = i}
Definíció. Legyen S egy A=(v1:A1 , ... , vn:An , v:T) állapottér feletti program. Az S program alapállapotterének leszűkítésén azt a programot értjük (jelöljük ezt S’-vel), amelynek alap-állapottere a C=(v1:A1 , ... , vn:An), és minden cC-re
S’(c) = {
C aA: c=prC(a) és S(a) A }
{ < c, > C aA: c=prC(a) és S(a) A
}
A program alap-állapottere egy önkényesen kijelölt halmaz. Kibővítése nem változtatja meg a program működését, sőt a leszűkítése sem, ha az alap-állapottérből elhagyott változó legelső használata előtt kibővül vele az aktuális állapottér, és a program befejeződésekor törlődik.
6. Megoldás fogalma Nem változott meg az alábbi két fogalom definíciója. Definíció. Legyen A egy állapottér. A p(S)AA relációt az A állapottér feletti S program programfüggvényének (hatásának) nevezzük, ha 1.
p(S)={
aAS(a) A }
2. minden a
p(S)-re:
p(S)(a) = { bAvan olyan S(a), hogy ||=b }
Definíció. Legyen az F egy A állapottér feletti feladat, az S az A állapottér feletti program. Az S program megoldja az F feladatot, ha
1.
F p(S’)
2. minden a F-re: p(S’)(a)F(a) A megoldás definíciója feltételezi, hogy a feladat állapottere megegyezik a program alapállapotterével. De vajon megoldható-e egy feladat annak állapotterétől eltérő alap-állapotterű programmal? A programozási gyakorlatban sokszor előfordul, hogy egy feladatot egy olyan programmal akarunk megoldani, amelyik állapottere nem azonos a feladatéval, bővebb vagy szűkebb annál, esetleg más változóneveket használ. Említettük már, hogy egy program alap-állapotterét megállapodás alapján jelölhetjük ki. Ha az a célunk, hogy egy adott feladatot oldjunk meg egy programmal, akkor először azt kell megvizsgálni, hogy a program alap-állapottere hozzáigazítható-e a feladat állapotteréhez. Ehhez a korábban bevezetett változó-átnevezést, alap-állapottér bővítést és szűkítést használhatjuk, hiszen ezek a program működését nem változtatják meg. A cél az, hogy a program alapváltozói a feladat (bemenő és eredmény) változói legyenek, azaz a program alap-állapottere a feladat állapotterével egyezzen meg. Ha ez sikerül, akkor a megoldás tényét a fenti definícióval már ellenőrizhetjük. Ha a feladat állapotteréhez „hozzáigazított” program megoldja a feladatot, akkor az eredeti program is megoldja azt. Az eredeti és a hozzáigazított programok működése azonos. Ahhoz azonban, hogy egy program egy másik programhoz hasonlóan ugyanazon feladatokat tudja megoldani elegendő, ha a programok ekvivalensek. Definíció. Legyenek S1 és S2 programok olyanok, amelyek alap-állapotterei (megfelelő változóátnevezés, kibővítés illetve leszűkítés után) megegyeznek. Az S1 és S2 programok ekvivalensek, ha a közös alap-állapottéren felírt változataik S’1 és S’2 programfüggvénye megegyezik, azaz p(S’1) = p(S’2). Ez a fogalom reflexív, szimmetrikus és tranzitív, tehát a programok halmazán egy ekvivalencia osztályozást határoz meg. Ennek az a következménye, hogy egy program akkor old meg egy feladatot, ha a program ekvivalencia-osztályának valamelyik programja, például a feladat állapotterét alap-állapottérként használó vele ekvivalens program megoldja azt.
7. Következmények A programozási modell fenti módosítása a módosítások a modell többi fogalmát, köztük talán a legfontosabbat, a megoldás definícióját nem érintik. Részletesen bebizonyítandó ugyan, de az előzetes vizsgálatok szerint a modell keretén belül korábban bizonyított eredmények megmaradnak. Ugyanúgy lehet például a feladatra kimondani és bizonyítani a specifikáció alaptételét, bevezetni az elemi programokat és programszerkezeteket, bizonyítani a levezetési szabályokat. Két új elemi programot kell bevezetni: új változó létrehozása illetve megszűntetése. Lényeges egyszerűbb lett viszont annak eldöntése, ha egy feladatot egy olyan programmal akarunk megoldani, amelyik állapottere nem azonos a feladatéval, bővebb vagy szűkebb annál, esetleg más változóneveket használ.
Megnyílt a lehetőség az alprogramok absztrakt definíciója előtt. Az alprogram hívása egy speciális utasításként fogható fel, amely képes újabb változókat végrehajtás közben létrehozni. Be lehet vezetni az alprogramra nézve lokális változókat, ezek között a paraméterváltozókat, és az alprogramok rekurzív hívását is meg lehet engedni. Ennek részletes kidolgozása későbbi feladat. A programozási modell fenti változtatása visszacsempészte az alapvetően statikus szemléletbe a program dinamikus természetét. Miközben a megoldás vizsgálatához továbbra is a statikus szemléletet alkalmazhatjuk, a programnak a gyakorlat szempontjából természetesebb dinamikus viselkedése megjelenhet a modellben.
8. Irodalom 1. Dijkstra E.W., ``A Discipline of Programming'',Prentice-Hall, Englewood Cliffs, 1973. 2. Dijkstra E.W. and C.S. Scholten, ``Predicate Calculus and Program Semantics'', SpringerVerlag, 1989. 3. Fóthi Ákos: Bevezetés a programozáshoz. ELTE Eötvös Kiadó. 2005. 4. Gries D., ``The Science of Programming'', Springer Verlag, Berlin, 1981. 5. Hoare C.A., „Proof of Correctness of Data Representations}, Acta Informatica” (1972), 271-281. 6.
„Workgroup on Relation Models of Programming: Some Concepts of a Relational Model of Programming,Proceedings of the Fourth Symposium on Programming Languages and Software Tools, Ed. prof. Varga, L., Visegrád, Hungary, June 9-10, 1995. 434-44.”
