Tartalom
Programozási modellnek nevezzük azt a matematikai modellt, amely megadja feladatok és programok szemantikai jelentését, konstrukciós műveleteket definiál feladatok és programok felett, valamint megadja, hogy egy program mikor old meg egy feladatot. Relációs modellről beszélünk, ha a szemantikai tartományok elemei relációk.
Gondolkodásunk során a programozási feladat [[???Fót 83]] fogalmából indulunk ki. Programozási feladatot mindig egy állapottéren [[???Dij 76]] fogalmazunk meg. A feladat megfogalmazásához tehát meg kell alkotnunk a feladat matematikai modelljétA modell szót általános értelemben használjuk. Ha a matematikai logikában, a modellelméletben használt modellfogalomra gondolunk, akkor erre külön hivatkozunk. Egy feladat megfogalmazása nem köthető pl. egy rögzített temporális logikai struktúrához, mert ez esetben a feladat már nem fogalmazható meg függetlenül az időstruktúrát definiáló programtól. A feladatot nem azonosítjuk az őt leíró formulák halmazával, mint szintaktikus egységekkel sem, ugyanis egy interpretálatlan formulahalmaz minden interpretációban más és más szemantikai jelentést hordoz. A feladatot mindig egy rögzített állapottér felett, azon értelmezett relációk segítségével adjuk meg., absztrakcióra van szükség. A feladat megfogalmazásához vezető utat most nem vizsgáljuk.Nem vizsgáljuk azt, hogy egy feladat formális alakja valóban azt a feladatot írja-e le, amit valamilyen természetes nyelven megfogalmaztak. A választott programozási modell keretein túlmutat ennek a kérdésnek a vizsgálata.
Első példánk E. W. Dijkstrától származik, aki az operációs rendszerek tárgy tanítása során a folyamatok közötti kölcsönös kizáráson alapuló erőforrásmegosztás elvét szemléltette vele. Ez a példa öt, egymással együttműködő párhuzamos folyamatból álló rendszert modellez. A történet szerint egy asztal körül öt filozófus ül, akik egy nagy közös tálból vehetnek maguknak makarónit. Ahhoz, hogy a makaróni a tányérba kerüljön két villára van szükség. A tálat többen is használhatják egyszerre, de az étkezéshez szükséges villák midegyikére külön-külön teljesülnie kell, hogy egyszerre csak egy filozófus használatában lehetnek. Minden filozófus számára két villa érhető el, ezek azonban olyan villák amelyeket szomszédai is szeretnének használni. Ha egy filozófus felemeli az asztalról bal- és jobboldali villáját és eszik, akkor egyik szomszédja sem rendelkezhet az étkezéshez szükséges két villával. Egyidejűleg csak egymással nem szomszédos filozófusok étkezhetnek .
Jelöljük az 
. filozófust 
-vel, az egyes állapotokat pedig a kezdőbetűjükkel:
gondolkodik:
, villákat
tart a kezében:
, eszik:
,
otthon van:
. A következőkben példákat mutatunk a filozófusok viselkedésére
vonatkozó specifikációs követelmények megfogalmazására.
Az „amíg nem” (jelölés: 
) típusú kikötésekkel egyes állapotátmeneteket tilthatunk. Megkövetelhetjük,
hogy minden filozófus gondolkodik, amíg villát nem tart a kezében vagy haza
nem ért: 
. Ez azt jelenti, hogy a gondolkodás állapotát nem követheti
közvetlenül az étkezés állapota. Kikötjük azt is, hogy a
villák kézben tartását csak az evés állapota követheti:
, a villák megszerzése után nem szabad sem hazamenni, sem
gondolkodni. Szigorúbb kikötést tehetünk oly módon, hogy a
megengedett állapotváltozások bekövetkezését elő is írjuk:
.
Az étkezést előbb utóbb fel kell váltania a gondolkodásnak.
Lazább kapcsolatot is megkövetelhetünk állapotok között:
, a
gondolkodás állapotát előbb utóbb elkerülhetetlenül követi, hogy a
filozófus otthon van. Invariáns tiltja, hogy szomszédok egyszerre étkezzenek:
.
Fixpont kikötéseket alkalmazunk arra, hogy előírást
tegyünk arra az esetre, ha a rendszer nyugalmi állapotba jut:
. A
kikötés szerint, ha további állapotváltozás nincs, akkor minden
filozófus otthon van. Megkövetelhetjük, hogy egy állapotból
elkerülhetetlen legyen a nyugalmi állapot elérése, a terminálás.