Programozás | Programozás-elmélet » Programozás-elmélet tételek

1. Folyamatábra-programok és -sémák Egy S folyamatábra-séma ΣS ábécéje az alábbi szimbólumhalmaz valamely véges részhalmaza: 1. Konstansok: fin (i≥1, n≥0): n-argumentumú függvénykonstansok; fi0-t elemkonstansnak nevezzük, és ai-vel jelöljük. pin (i≥1, n≥0): n-argumentumú relációkonstansok; pi0: ítéletkonstans. 2. Elemváltozók: xi: input változók, yi: programváltozók, zi: output változók. A ΣS-beli x input változók, y programváltozók és z outputváltozók száma legyen rendre a,b és c, ahol a,b,c≥0. Egy ΣS fölötti τ term a áll elő. ΣS elemváltozóiból, elemkonstansaiból és függvényváltozóiból a szokásos kompozícióval Egy ΣS fölötti A atomi formula vagy egy pi0 ítéletkonstans, vagy egy pin(t1,.,tn) alakú kifejezés, ahol n≥1 és t1,,tn ΣS fölötti termek. A ΣS fölötti utasítások a következő alakúak lehetnek: 1. kezdőutasítás: 2. 5. értékadás: 3. vizsgálat: 4. végutasítás:

végtelen ciklus utasítás: Egy ΣS fölötti folyamatábra-séma olyan véges, ΣS fölötti utasításokból konstruált folyamatábra, amelyben egy kezdőutasítás van, és minden értékadás és vizsgálat rajta van egy, a kezdőutasításból valamely végutasításhoz vagy végtelen ciklus utasításhoz vezető úton. Egy S folyamatábra-séma I interpretációi a következőkből állnak: 1. Egy D nemüres halmazból, amelyet az interpretáció alaphalmazának nevezünk; 2. A ΣS-beli konstansokra vonatkozó hozzárendelésekből: a) minden ΣS-beli fin függvénykonstanshoz hozzárendelünk egy Dn-t D-be leképező totális függvényt (ha n=0, az fi0 elemkonstanshoz D valamely rögzített elemét rendeljük); b) minden ΣS-beli pin relációkonstanshoz hozzárendelünk egy Dn-t {igaz, hamis}-ba képező totális relációt (ha n=0, a pi0 ítéletkonstanshoz az igaz vagy a hamis igazságértéket rendeljük). A P=<S, I> párt, ahol S folyamatábra-séma, I pedig

az S egy interpretációja, folyamatábra-programnak nevezzük. Az S input változóinak x vektorához megadva valamely ξ∈Da input értéket, a program végrehajtható. <P, ξ> kiszámítása úgy történik, hogy az x programváltozók a ξ értékeket kapják, a kezdőutasításnál az y programváltozók a τ(ξ) értékeket kapják. A kiszámítás véget ér, mihelyt egy végutasításhoz vagy végtelenciklusutasításhoz jutunk: az első esetben a végutasítás eredményeképpen az output változók értéke z=ζ∈Dc lesz, akkor azt mondjuk, hogy a program értéke (P(ξ)=val <P, ξ>) definiált, és P(ξ)=ζ; minden más esetben P(ξ) definiálatlan. A program tehát egy Da-t Dc-be leképező parciális függvényt reprezentál. Egy P program a) megáll, ha P(ξ) definiált minden ξ∈Da-ra; b) divergál, ha P(ξ) definiálatlan minden ξ∈Da-ra. Egy S séma a) megáll, ha <S,I> megáll S minden I interpretációja esetén; b) divergál, ha <S,I>

divergál S minden I interpretációja esetén. Az S és S sémát kompatibilisnek nevezzük, ha az input változók x vektora és az output változók z vektora megegyezik. Az <S,I> és <S,I> programot kompatibilisnek nevezzük, ha S és S kompatibilis, továbbá az I és I interpretációk alaphalmaza megegyezik. A P és P programok ekvivalensek, ha kompatibilis, és P(ξ)≡P(ξ). Az S és S kompatibilis sémák ekvivalensek, ha S és S minden I interpretációja esetén <S,I> és <S,I> ekvivalensek. A P és P programok izomorfak, ha kompatibilisek, és minden ξ∈Da esetén P(ξ) és P(ξ) kiszámítási sorozata megegyezik.Az S és S kompatibilis sémák izomorfak, ha S és S minden közös I interpretációja esetén <S,I> és <S,I> izomorf. Egy S séma Herbrand-univerzuma (HS) a következő halmaz: 1. ha xi input változója S-nek, és ai az S-ben szereplő elemkonstans, akkor "xi" és "ai" elemei HS-nek; 2. ha fin az

S-ben előforduló n-argumentumú függvénykonstans, és "t1",,"tn" HS-beli elemek, akkor "fin(t1,.,tn)" is eleme HS-nek Vagyis: HS={τ(x) }. Egy S séma Herbrand-interpretációja (I*) az a HS alaphalmazú interpretáció, amelyre teljesülnek a következő feltételek: 1. S minden ai elemkonstansához az "ai" HS-beli elem legyen rendelve; 2. S minden fin függvénykonstansához az a HS fölötti n-argumentumú függvény, amely tetszőleges "t1",,"tn" HS-beli jelsorozatokat az "f(t1,.,tn)" HS-beli jelsorozatra képez le (Az S relációkonstansaira nincs semmiféle megkötés.) Luckham-Park-Paterson tétel: 1. Tetszőleges S séma akkor és csak akkor áll meg/divergál, ha val <S,I*,"x"> definiált/definiálatlan S minden I Herbrand-interpretációja esetén. 2. Tetszőleges S és S kompatibilis séma akkor és csak akkor ekvivalens egymással, ha

val<S,I*,"x">≡val<S,I,"x"> S és S minden I Herbrand-interpretációja esetén. 3. Tetszőleges S és S kompatibilis séma akkor és csak akkor izomorf egymással, ha S és S minden I* Herbrandinterpretációja esetén <S,I,"x"> és <S,I,"x"> kiszámítási sorozata megegyezik. Egy S sémát szabadnak nevezünk, ha folyamatábráján minden, a kezdőutasításból kiinduló véges út kezdőszelete valamely kiszámításnak. 1. A szabad sémák megállási problémája megoldható: egy szabad séma pontosan akkor nem áll meg, ha szerepel benne végtelenciklus-utasítás, vagy folyamatábrája tartalmaz ciklust.) 2. A szabad sémák divergálási problémája megoldható: egy szabad séma pontosan akkor nem divergál, ha tartalmaz végutasítást. 3. Az, hogy egy séma szabad, parciálisan sem dönthető el 4. Nem ismeretes, hogy a szabad sémák ekvivalenciaproblémája megoldható-e 5. A szabad sémák

izomorfizmus-problémája megoldható Egy ΣT véges ábécé fölötti T faséma olyan (esetleg végtelen), ΣT fölötti utasításokból álló folyamatábra, amelynek gráfja fa, azaz: 1. pontosan egy kezdőutasítást tartalmaz; 2. minden egyes utasítása pontosan egy útból érhető el a kezdőutasításból (nincs benne csomópont); 3. levelei végutasítások vagy végtelenciklus-utasítások A véges fasémák megállási problémája, divergálási problémája, valamint ekvivalencia- és izomorfia-problémája megoldható. Minden folyamatábra-sémához megadható vele ekvivalens szabad faséma. Minden megálló folyamatábra-sémához megadható vele ekvivalens véges szabad faséma. Input feltételnek nevezzük azt a Dx feletti ϕ(x) relációt, amely leírja Dx inputként használható elemeit. A Ψ(x,z) output feltétel egy Dx×Dz feletti reláció; leírja azt az input és output változók közötti összefüggést, amelyet az input és output változók értékeinek

a program befejeződésekor ki kell elégíteniük. P parciálisan helyes ϕ-re és Ψ-re nézve, ha minden olyan ξ inputra, amelyre ϕ(ξ) teljesül és P(ξ) definiált, Ψ(ξ,P(ξ)) teljesül. P totálisan helyes ϕ-re és Ψ-re nézve, ha minden olyan ξ inputra, amelyre ϕ(ξ) teljesül, P(ξ) definiált, és Ψ(ξ,P(ξ)) teljesül. P megáll ϕ-re nézve, ha minden olyan ξ inputra, amelyre ϕ(ξ) teljesül, P(ξ) definiált. Ha egy program totálisan helyes, akkor parciálisan is helyes. A parciális helyességből és a megállásból következik a totális helyesség. Parciális helyesség bizonyítása Floyd-féle induktív állítások módszere: 1. vágási pontokat helyezünk el a programban a) a kezdőutasításból induló élen (kezdőpont); b) a végutasításokhoz vezető éleken (végpontok); c) minden ciklusban elhelyezünk legalább egy vágási pontot (belső pontok). Csak azokat a szakaszokat vesszük figyelembe, amelyek vágási ponttól vágási pontig

terjednek, és nincs rajtuk közbenső vágási pont (közvetlen út). Legyen α egy i-ből j-be vezető út Jelentse Rα(x,y) azt a feltételt, amely mellett a vezérlés végighalad az α úton, az rα(x,y) függvény pedig azt a transzformációt, amelyet az α út által leírt programrész okoz az y változókon. Ezek előállítására a visszafelé helyettesítés módszere szolgál. 2. A program minden i vágási pontjához hozzárendelünk egy pi(x,y) induktív állítást, amely jellemzi a változók közötti összefüggést az i pontban. A kezdőponthoz az input feltételt, míg a végpontokhoz az output feltételt rendeljük. 3. Minden α úthoz megszerkesztjük a megfelelő helyességi feltételt: ∀x,y[pi(x,y) ∧ Rα(x,y) pj(x, rα(x,y))]. Ha j végpont, akkor a helyességi feltétel ∀x,y[pi(x,y) ∧ Rα(x,y) Ψ(x, rα(x,z))] lesz, míg ha i kezdőpont, akkor ∀x[ϕ(x) ∧ Rα(x) pj(x, rα(x))]. Ez a helyességi feltétel egyszerűen azt állítja, hogy ha pi

igaz x és y olyan értékeire, amelyek mellett az α útban leírt programrészlet végrehajtódik, akkor pj igaz lesz a programszakasz végrehajtásával kapott x, y értékekre. Ha P-re, ϕ-re és Ψ-re elvégezzük az 1-3. lépéseket és minden helyességi feltétel igaz, akkor P parciálisan helyes ϕ-re és Ψ-re. Mivel minden közvetlen útra bebizonyítottuk a helyességi feltételt, ezért a kezdőpontból a végpontba vezető út sorozat esetén a végponthoz rendelt Ψ helyességi feltétel is igaz lesz. Manna-féle részcél-módszer: 1. Vágási pontok elhelyezése a Floyd-módszerrel megegyező módon 2. Részcélok vágási pontokhoz rendelése: a) a kezdőponthoz: ϕ(x)Ψ(x,z); b) belső pontokhoz: pi(x,y)qi(x,y,z); c) végponthoz: T. 3. Helyességi feltételek meghatározása a közvetlen utakra: a) belső pontból belső pontba: ∀x,y,z [pj(x, rα(x,y))qj(x, rα(x,y),z) ∧ Rα(x,y) (pi(x, rα(x,y))qi(x, y,z))]; b) kezdőpontból belső pontba: ∀x,z [pj(x,

rα(x,y))qj(x, rα(x,y),z) ∧ Rα(x,y) (ϕ(x)Ψ(x,z))]; c) belső pontból végpontba: ∀x,y [ Rα(x,y) (pi(x, rα(x,y))qi(x, y,z))]; d) kezdőpontból végpontba: ∀x [ Rα(x,y) ∧ ϕ(x)Ψ(x,z)]. Ha P-re, ϕ-re és Ψ-re elvégezzük az 1-3. lépéseket és minden helyességi feltétel igaz, akkor P parciálisan helyes ϕ-re és Ψ-re. Megállás bizonyítása Egy (W,<) parciálisan rendezett halmaz egy W nemüres halmazból és egy < bináris relációból áll, mely W elemein van értelmezve és tranzitív, aszimmetrikus és irreflexív. Egy (W,<) parciálisan rendezett halm,azt megalapozottnak nevezünk, ha nincs benne végtelen csökkenő sorozat. Megalapozott halmazok módszere: 1. Vágási pontokkal vágjuk fel a programban szereplő hurkokat, és minden i vágási ponthoz rendeljünk hozzá egy qi(x,y) állítást, amely a) minden olyan α, a kezdőpontból valamely j vágási pontba vezető közvetlen útra fennáll: ∀x[ϕ(x)∧Rα(x) qj(x, rα(x))] b)

minden olyan α, a i vágási pontból a j vágási pontba vezető közvetlen útra fennáll: ∀x,y[qi(x,y)∧Rα(x,y) qj(x, rα(x,y))] 2. Válasszunk egy (W, <) megalapozott halmazt és minden i vágási ponthoz rendeljünk egy ui(x,y) parciális függvényt, amely Dx×Dy-ból W-be képez és ∀x,y[qi(x,y) ui(x,y)∈W] 3. Minden olyan α, a i vágási pontból a j vágási pontba vezető közvetlen útra, amely része egy programhuroknak írjuk fel a megállási feltételt: ∀x,y{qi(x,y)∧Rα(x,y) [ui(x,y) > uj(x, rα(x,y))]} Egy adott P folyamatábra-programra és ϕ(x) inpput feltételre végezzük el az 1-3. lépéseket Ha az összes megállási feltétel igaz, akkor P megáll ϕ mellett. 2. While-programok Egy while-program véges sok, egymástól pontosvesszővel elválasztott utasításból áll: B0; B1;.; Bn, ahol B0 : START y←f(x), Bn : z←h(x) HALT És minden Bi (0<i<n) utasítás a következő utasítástípusok valamelyike: 1. értékadó utasítás:

y←g(x) 2. feltételes utasítás: if t(x,y) then B else B vagy if t(x,y) do B, ahol B és B tetszőleges utasítás. 3. ciklusutasítás: while t(x,y) do B, ahol B tetszőleges utasítás. 4. összetett utasítás: begin B;.;B(k) end, (i) ahol B tetszőleges utasítás. Parciális helyesség (Hoare módszer) Induktív kifejezés: {p(x, y)} B {q(x, y)}, ahol p, q relációk és B egy programszegmens. Az induktív állítás azt jelenti, hogy ha p(x, y) fennáll az x, y értékekre B végrehajtása előtt, és B végrehajtása befejeződik, akkor q(x, y) fenn fog állni a B végrehajtása után kapott x, y értékekre. A P program helyességének bizonyítása a {ϕ(x, y)} P {Ψ(x, y)} induktív kifejezés levezetéséből áll, amelyhez levezetési szabályok állnak rendelkezésre a következő alakban: α1 α és α 2 vagy 1 β β ahol α és α azok a feltételek, amelyek mellett a szabály alkalmazható, β a levezetett induktív 1 2 kifejezés. A feltételek vagy már

korábban levezetett induktív kifejezések vagy logikai kifejezések lehetnek, ezeket mint lemmákat külön kell bizonyítani. Levezetési szabályok: 1. értékadás-axióma: {p(x, g(x, y))} y ← g(x, y) {p(x, y)} 2. feltételes szabályok: {p ∧ t}B1{q} Žs {p ∧ ¬t}B2 {q} Žs {p ∧ t}B{q} Žs ( p ∧ ¬t ) q {p}if t do B {q} {p}if t then B1 else B2 {q} 3. {p ∧ t} B {p} {p} while t do B {p ∧ ¬t} 4. {p}B1 {q} Žs {q}B2 {r} {p}B1 ; B2 {r} 5. { p q Žs {q}B{r } p}B{q} Žs q r Žs {p}B{r} {p}B{r} while-szabály: kompozíciós szabály: következmény-szabályok: Adott egy P while-program, ϕ(x) input feltétel Ψ(x, z) output feltétel. Ha az előbbiekben leírt szabályok alkalmazásával sikerül levezetni a {ϕ(x, y)} P {Ψ(x, y)} kifejezést, akkor P parciálisan helyes ϕ-re és Ψ-re nézve. Totális helyesség (Dijkstra-féle leggyengébb előfeltétel-kalkulus) wp(B, q): az a leggyengébb előfeltétel, amely mellett B megáll és a megállás után q

teljesül. B totálisan helyes p-re és q-ra nézve, ha p wp(B, q). Alaptulajdonságok: a) wp(B, F) = F; b) wp(B, p∧q) = wp(B, p) ∧ wp(B, q); c) wp(B, p∨q) = wp(B, p) ∨ wp(B, q); d) ha p q, akkor wp(B, p) wp(B, q). Utasítások leggyengébb előfeltételei: a) wp(skip, q) = q; b) wp(B1;B2, q) = wp(B1, wp(B2, q)); c) wp(y←f(x, y), q(x, y)) = q(x, f(x, y)); d) wp(if t then B1 else B2, q) = wp(B1, q)∧t ∨ wp(B2, q)∧¬t = twp(B1, q) ∧ ¬twp(B2, q); e) wp(while t do B, q) = ∃i≥0: pi, ahol pi annak a leggyengébb előfeltétele, hogy B-t pontosan i-szer végrehajtva t már nem teljesül, de q teljesül. pi = ¬t∧q; pi+1 = t∧wp(B, pi). wdec(B, u) annak a leggyengébb előfeltétele, hogy B csökkenti u-t (u∈Z). Ha p∧twp(B1, q) és p∧¬twp(B2, q), akkor pwp(if t then B1 else B2, q). Ha p∧twp(B, q) és u≥0 és wdec(B, u), akkor pwp(while t do B, p∧¬t). Ha p∧twp(B, p) és pwp(while t do B, T), akkor pwp(while t do B, p∧¬t). A totális helyesség

bizonyításához a ϕwp(P, Ψ) kifejezést kell levezetni a fenti szabályok segítségével. 3. Rekurzív programok és sémák Egy S rekurzív séma ΣS ábécéje az alábbi szimbólumhalmaz valamely véges részhalmaza: 1. konstansok: fin függvénykonstansok pin relációkonstansok 2. változók: x1,., xa, y1,,yb, z elemváltozók Fi b-változós függvényváltozók. A ΣS feletti term és atomi formula ugyanaz, mint a folyamatábra-sémák esetén. konstans term: olyan term, amelyben Fi nem szerepel. Csak olyan atomi formulák megengedettek, amelyek konstans termekből állnak. Feltételes term: - minden term feltételes term - ω (a definiálatlanság szimbóluma) nem term, de feltételes term - ha A egy atomi formula, τ1, τ2 feltételes termek, akkor az if A then τ1 else τ2 szöveg feltételes term. S rekurzív séma: z = τ0(x, F), ahol F1(y) ← τ1(x, y, F), : Fn(y) ← τn(x, y, F). ahol τ0,., τn ΣS feletti feltételes termek Interpretáció: - alaphalmaz (D)

megadása; - minden fin függvénykonstanshoz hozzárendelünk egy ϕ: DnD totális függvényt; - minden pin relációkonstanshoz hozzárendelünk egy π: Dn{igaz, hamis} totális függvényt. Kiszámítási sorozat: α0,., αn elemei fin-ből, Fi-ből és D elemeiből álló termek, melyek tovább már nem egyszerűsíthetők. Egyszerűsítő műveletek: - fin kiszámítása, ha értéke D-beli; - az if A then τ1 else τ2 feltételes term esetén A kiszámítása után a kifejezés helyettesíthető τ1-gyel vagy τ2vel. α0 = τ0(αi, F) az összes lehetséges egyszerűsítés után. αi+1-et αi-ből úgy kapjuk, hogy vesszük a legelső, legbaloldalabbi Fi előfordulást, elvégezzük a programban előírt helyettesítést (az yi-k helyére a megfelelő argumentumok, az xi-k helyére pedig a ξi-k kerülnek. Ezek csak D-beli elemek lehetnek!), majd az így kapott termet egyszerűsítjük. Ha (αi) véges, és az utolsó eleme D-beli, akkor P(ξ) definiált, és értéke ez az

utolsó elem; minden más esetben P(ξ) nem definiált. Minden folyamatábra-sémához megadható vele ekvivalens rekurzív séma. (Csak 1 outputos folyamatábra-sémára) Vágási pontokat helyezünk el, és minden belső ponthoz hozzárendelünk egy függvényváltozó-értéket, melynek értéke a leendő output érték, argumentumai pedig a programváltozók tartalma. A következő rekurzív sémához nem adható meg vele ekvivalens folyamatábra-séma: z = F(a), ahol F(y) ← if p(y) then f(y) else h(F(g1(y)), F(g2(y))). 4. Nemszekvenciális (párhuzamos) programok Általában több erőforrás (proceszor, memória, perifériák, háttértárak stb.) áll rendelkezésre, mint amennyire egy programnak szüksége van. Ezért lehetőség van arra, hogy egyszerre több program is jelen legyen Ezek a programok osztoznak az erőforrásokon; váltakozva jutnak hozzá a központi egységhez, szinte párhuzamosan hajtódnak végre. Az ilyen programok rendszere egyetlen virtuális

párhuzamos rendszert képez. Ez a rendszer igen laza rendszer, az erőforrások megosztását az operációs rendszer végzi; az egyes programok úgy készíthetők el, mintha egyedül lennének jelen a gépen. Az olyan rendszerek, amelyek komponensei között sokkal szorosabb a kapcsolat (pl. folyamatvezérlési programrendszer) az erőforrások megosztását feltételezve jöttek létre, egymással üzenetet váltanak, egymás szolgáltatásait igénybe veszik, szolgáltatásokra várnak. Ha egy ilyen programrendszer egyprocesszoros gépen fut, akkor a párhuzamosság virtuális, míg többprocesszoros gépen a rendszer bizonyos részei ténylegesen párhuzamosan hajtódnak végre. A párhuzamos program egy rendszer, amely az erőforrások ls a szekvenciális programok egy egysége. A végrehajtás alatt lévő programot folyamatnak nevezzük. A párhuzamos renszer állapotát a folyamatok és az erőforrások viszonya határozza meg. A folyamatok ezt az állapotot utasításokon

keresztül megváltoztatják A folyamatnak azon részei, amelyek nem tartalmaznak rendszerállapotot megváltoztató utasításokat, egymással párhuzamosan végrehajthatók. Az erőforrások a használat szempontjából lehetnek: 1. kizárólagos használatú; 2. megosztható A megosztható erőforrásokat egyidejűleg több folyamat is használhatja. A kizárólagos használatú erőforrások belső állapotát a folyamatok megváltoztatják, ezért egyszerre egynél több folyamat nem használhatja. Az erőforrások használatának ajánlott rendje: 1. az erőforrás igénylése; 2. az erőforrás lekötése; 3. az erőforrás felszabadítása A folyamatoknak két állapota lehet: 1. aktív állapot: minden olyan erőforrást lekötve tart, amelyre igényét bejelentette; 2. blokkolt állapot: erőforrás felszabadulására vár Alapproblémák Holtpont-mentesség: A holtpont olyan állapot, amikor a rendszert alkotó folyamatok közül kettő vagy több folyamat várakozik a

végtelenségig egy olyan eseményre, amelyik soha nem következik be. Holtpont esetén a rendszer működésképtelenné válik, csak külső (pl. operátori) beavatkozással indítható tovább Az olyan rendszert, amelyben holtpont-állapot nem következhet be, holtpont-mentesnek nevezzük. Példa: Adott két folyamat és két erőforrás. Az első folyamat az 1, a második folyamat a 2 erőforrást tartja lekötve Ha mindkét folyamat bejelenti igényét a másik által lekötve tartott erőforrásra mielőtt a sajátját elengedné, előáll a holtpont-állapot. Kölcsönös kizárás: Vannak olyan erőforrások, amelyeket egyidejűleg egynél több folyamat nem használhat. A rendszernek olyannak kell lennie, hogy a folyamatok kölcsönösen kizárják egymást az ilyen erőforrások használatából. A folyamatoknak vannak kritikus szakaszaik A kölcsönös kizárás azt jelenti, hogy legfeljebb egy folyamat tartózkodhat kritikus szakaszban. Primitív utasítás: olyan

utasítás, amelynél a kölcsönös kizárást a hardver végzi. Jele: [ ] Szinkronizáció: A rendszer folyamatai általában közös feladatot oldanak meg, és ennek érdekében együttműködnek. Ez együttműködés során egymásnak jelzéseket, üzeneteket küldenek. Rendszerint vannak olyan szakaszok, amelyekbe a folyamatok csak akkor léphetnek be, ha erre egy másik folyamattól engedélyt kapnak. Ily módon a rendszert alkotó folyamatoknak szinkronban kell működniük. Dijkstra-féle szemaforok A Dijkstra-féle szemafor (s) a folyamatok egy egész értékű közös változója, amelyet a folyamatok várakozó sorához (például egy adott tipusú erőforrásra várakozók sorához) kölcsönösen és egyértelműen hozzárendelünk. Az s szemafor kezdeti értéke a folyamatok indulásakor pozitív érték, rendszerint 1. A folyamatok egymásnak jelzéseket küldhetnek a rendszer állapotát megváltozztató utasítások kiadása előtt és után a szinkronizációs

utasításokkal: 1. P(s) beléptető művelet: [ s ← s-1; ha s<0, akkor a folyamat belép a várakozók sorába] 2. V(s) kiléptető művelet: [ s ← s+1; ha s≥0, akkor egy folyamat kilép a várakozók sorából] A kiléptető műveletben nem rögzített az a stratégia, amellyel a várakozók sorából a folyamat kiválasztható. A sorrendet a beütemező stratégiák rögzítik. A kölcsönös kizárás megvalósításához minden közös erőforráshoz felveszünk egy szemafort, s=1 kezdőértékkel, majd minden folyamatot a következő elv szerint valósítunk meg: .; P(s); kritikus szakasz; V(s); A szemafor felhasználható szinkronizálásra is. Példa: termelő-fogyasztó rendszer. Adott egy n-elemű puffer, egy termelő és egy fogyasztó folyamat A termelő nem termelhet többet a puffer méreténél, a fogyasztó nem fogyaszthat gyorsabban a termelésnél. Megvalósítása: s szemafor: a pufferben lévő elemek száma (s=0 kezdőérték); r szemafor: a pufferben

lévő üres helyek száma (r=n kezdőérték). termelés: .termelés; P(r); az adat elhelyezése; V(s); fogyasztás: P(s); elem kiolvasása és törlése; V(r); fogyasztás. 5. Dijkstra-féle nemdeterminisztikus programok A nemdeterminisztikus programok a while-programok bővítései a következő két utasítással: 1. szelekciós utasítás: if t1B1 � . � tnBn fi ahol ti őrfeltétel, Bi tetszőleges programszegmens. Kiválasztunk egy igaz értékű őrfeltételt és végrehajtjuk a hozzá tartozó programszegmenst. A kiválasztás véletlenszerű, általunk ismeretlen Ha nincs igaz értékű őrfeltétel, a program abortál. 2. repetatív utasítás: do t1B1 � . � tnBn od Kiválasztunk egy igaz értékű őrfeltételt és végrehajtjuk a hozzá tartozó programszegmenst. Ezt addig ismételjük, amíg az összes őrfeltétel hamissá nem válik. Leggyengébb előfeltétel-kalkulus nemdeterminisztikus programokra wp(B, q) annak a leggyengébb előfeltétele, hogy B

végrehajtását elkezdve a végrehajtás biztosan befejeződik és q biztosan teljesül. Alaptulajdonságok: - wp(B, F) = F; - ha q1q2, akkor wp(B, q1)wp(B, q2); - wp(B, q1∧q2) = wp(B, q1)∧wp(B, q2); - wp(B, q1∨q2) wp(B, q1)∨wp(B, q2). Utasítások wp értékei: - wp(skip, q) = q; - wp(y← f(x, y), q) = q(x, f(x, y)); - wp(B1;B2, q) = wp(B1, wp(B2, q)); - wp(if t1B1 � . � tnBn fi, q) = n tt ∧ ∧ (t i wp (Bi , q )), ahol tt = ∨ t i . n i =1 i =1 - wp(do t1B1 � . � tnBn od, q) = ∃i≥0: pi, ahol pi annak a leggyengébb előfeltétele, hogy a végrehajtás legfeljebb i lépésen belül befejeződik és q biztosan teljesül. p0 = ¬tt ∧ q; pi+1 = pi ∨ wp(IF, pi), ahol IF ugyanaz mint a do.od, csak iffi-vel Ha p∧twp(B1, q) és p∧¬twp(B2, q), akkor pwp(if t then B1 else B2, q). Ha ∀i: p∧tiwp(B, q), akkor p∧ttwp(IF, q). Ha p∧twp(B, p) és wdec(B, u) és u≥0, akkor pwp(while t do B, p∧¬t), ahol wdec(B, u) annak a leggyengébb

előfeltétele, hogy B biztosan csökkenti u-t legalább 1-gyel. 6. Owicki-Gries-féle párhuzamos programok A while-programot két utasítással bővítjük: 1. párhuzamosan végrehajtható utasítások: cobegin B1 ||.|| Bn coend, ahol Bi párhuzamos programszegmens. Az n ág szimultán hajtódik végre, a végrehajtás sebessége nemdeterminisztikus. 2. várakoztató utasítás: await t then B, ahol t feltétel, B szekvenciális programszegmens. Addig várakozik, amíg t igazzá nem válik, majd végrehajtja B-t. Egy szekvenciális programszegmens végrehajtását oszthatatlannak nevezzük, ha biztosítani tudjuk a végrehajtásának más ágak végrehajtásától való függetlenségét. Kifejezések kiértékelése és az értékadó utasítások oszthatatlanok. Ezért kifejezésben vagy értékadó utasításban olyan változó, amelyre más ágakban értékadó utasítás vonatkozik, egyféle, és legfeljebb egyszer szerepelhet. Levezetési szabályok 1. A megvárakoztatás

következtetési szabálya: {p ∧ t} B {q} {p} await t then B {q} 2. A párhuzamosság következtetési szabálya: {p1 }B1 {q1 }{p n }Bn {q n } Žs ezek interferen ciamentese k {p1 ∧  ∧ p n } cobegin B1  Bn coend {q1 ∧  ∧ q n } Legyen S egy utasítás, pre(S) egy előfeltétel, {p}B{q} egy igaz induktív kifejezés a levezetésével. Azt mondjuk, hogy S nem interferál pre(S) mellett a {p}B{q} levezetésével, ha - {pre(S)∧q} S {q} {pre(S)∧pre(B)} S {pre(B)} a B minden olyan B részutasítására, amely nem része await utasításnak, és ppre(B)p. A {p1}B1{q1},., {pn}Bn{qn} induktív kifejezéseket interferencia mentesnek nevezzük, ha minden i-re Bi minden await vagy await-en kívüli S értékadó utasítása nem interferál a {pj}Bj{qj} j≠i induktív kifejezések levezetésével a pre(S) előfeltétel mellett. A B programszegmensben szereplő X változó-halmazt segédváltozó-halmaznak nevezzük, ha X elemei B-ben csak olyan kifejezésekben

szerepelnek, amelyek X elemeire vonatkozó értékadások jobboldalai. Legyen X egy segédváltozó-halmaz B-ben; p, q elő- és utófeltételek, amelyek nem tartalmaznak X-beli változókat. Ekkor: {p}B{q} , ahol B-t B-ből úgy kapjuk, hogy az X elemeit tartalmazó utasításokat töröljük. {p}B {q} Szemaforok implementálása Egyszerű szemafor: P(s): await s>0 then s:=s-1; belépés V(s): await T then s:=s+1; kilépés. Dijkstra-szemafor: w[i]: folyamatonként egy-egy tömbelem, amely a folyamatok várakozását fejezi ki. Kezdetben minden i-re w[i]=F. P(s): await T then begin s:=s-1; if s>0 then w[ez a folyamat]:=T end; await ¬w[ez a folyamat] then skip; V(s): await T then begin s:=s-1; if s<0 then begin egy w[i]=T kiválasztása; w[i]:=F end; end;