Informális vs. formális probléma leírás
Valós világ (Domain) (Hibás eredmény)
Ködös határ (Félreértés, hiba)
Formális világ
(Megoldás)
A specifikáció csak nagyvonalakban írja le a valóságos problémát, amit a szoftver fejlesztőnek meg kell értenie.
Probléma dekompozíció, struktúrák leírása • A valóságos problémákat egyszerűbb részproblémákra kell felbontani • A problémának és a részproblémának általában ugyanazok a domainjei, vagyis azonos világban játszódnak le • A közös domaint különböző részproblémákban különböző szempontok szerint vizsgáljuk és írjuk le • A probléma dekomponálásnak hatását illusztrálja a következő példa…
Példa: öntözőrendszer zsilip problémája • Valóságban • Egy kis zsilipről van szó, ahol a zsilipkapu felemelkedik / leesik, melyet egy számítógép vezérel. • A zsilipkaput egy forgó csavarral mozgatják fel / le, egy kis motor segítségével. • Motorvezérlő elektromos jelek: be, ki, jobbra forog, balra forog • Zsilip tetején és alján egy-egy érzékelő: top, bottom • top: a kapu teljesen nyitva • bottom: a kapu teljesen zárva • Zsilip és számítógép között • 4 pulzus vonal vezet a motorhoz a számítógépből és • 2 állapot vonal vezet a kapu szenzoroktól a számítógépbe. • Követelmény • A zsilipkapu óránként 10 percig legyen nyitva, egyébként zárva • Megkövetelt jelenségek: kapu nyitva, kapu csukva • Specifikációs jelenségek: motor vezérlő jelei, szenzorok állapotai.
Példa: öntözőrendszer zsilip problémája • A "világunk" (domain) tulajdonságai, melyeket a gép tervezésénél figyelembe kell venni • A motor az állapotának megváltozásával válaszol a hozzá érkező külső jelre. • A zsilip mechanikus része az állapotát (emelkedik, esik), aszerint változtatja, hogy a motor áll, vagy egyik vagy másik irányba forog. • A szenzorok állapotai és a kapu vertikális pozíciói közötti kapcsolatok. • A zsilip mechanikus részeinek az állapot változásait (áll, emelkedik, süllyed) az vezérli, hogy a motor áll, vagy forog és milyen a forgási iránya. • A vezérlő gép specifikációjának ezeket formálisan kell rögzítenie.
Példa: öntözőrendszer zsilip problémája • A kapu állapotai: nyitva, zárva, emelkedik, süllyed • Specifikációs jelenségek (kapura vonatkozóan) (Kapu állapotai, motor jelei, top és bottom szenzor jelei közötti kapcsolat). • emelkedik: a motor elindul az óramutató járásával egyező irányban. • nyitva:
a fenti irányú haladásnál a top szenzor jelzést ad.
• süllyed:
a motor az óramutató járásával ellenkező irányban forog
• zárva:
ellenkező irányú haladásnál a bottom szenzor jelt ad.
Példa: öntözőrendszer zsilip problémája • Nyilvánvaló ellentmondások kezelése • A fizikai eszközök nem olyan megbízhatóak, ahogyan gondoljuk… • Elszakadhat a kábel, • leéghet a motortekercs, • a rozsda tönkreteheti a vasból készült alkatrészeket stb. • A vezérlő gép viselkedésénél ezeket figyelembe kell venni, a motor megállásainak okai közé ezeket be kell venni. • További lehetséges hibás jelenségek • Top és Bottom szenzor egyszerre jelez, • Zsilip emelésnél n mp. elteltével sem jelez a Top szenzor, • Zsilip emelésnél x mp. eltelte után is jelez a Bottom szenzor, • Zsilip leengedésnél m mp. eltelte után is jelez a Top szenzor, • Zsilip leengedésnél y mp. elteltével sem jelez a Bottom szenzor. szenzor • Megoldás: auditáló program használata
Auditáló program közös domain esetén • Az auditáló program konkurens módon fut a vezérlő programmal. • A közös erőforrásokhoz való hozzáférésnél kölcsönös kizárást kell biztosítani. • A két program egymással kommunikál • Hiba detektálása esetén az auditálható program jelzést küld a vezérlő gépnek. • A vezérlő gép az auditáló program jelzésére leállítja a motort és az előre megadott tevékenységeket elindítja.
Objektumok azonosítása • Különbséget kell tenni • Követelmény jelenségeinek leírásában szereplő azonosítók (A lift esetében: hol(f), fel, le) és • specifikációs jelenségek leírásában szereplő azonosítók között (sensor(f) állapotai a lift domain esetén). n) • f az emelet azonosítója volt, ami az informális leírásokban is szerepelt. • „Érdekesség” Elektromos vezeték szakadás detektálása és nem kellő megerősítő ellenőrzése számos repülőgép szerencsétlenség okozója volt. Például: Elégett vezetékként érzékelték a dohányfüstöt.
Komplexitás „A számítógépek gyakran olyan komplexitást hoznak be a probléma világába, amellyel interakcióba lépnek.” •
Ennek okai 1. A szoftver bonyolultsága; 2. A probléma világával való együttműködés bonyolultsága; 3. Ezt a bonyolultságot a régi rendszerekben három tényező kontrol alatt tartotta. • • •
Maga a szoftver és annak kézi kezelése kisebb és egyszerűbb volt, mint a mai rendszerek. Nem volt lehetőség, talán igény sem rendszerek ambíciózus integrálására. A rendszerek működtetése emberi közreműködésre hagyatkozott (az operátor közbeavatkozott, ha abszurd viselkedést látott). Számos alkalmazásban megszűnt ez a biztosíték.
Verifikáció A géppel történő megoldás specifikációja (formális leírás) Verifikáció (formális igazolás) Specifikáció (igazolt, bizonyított) Kifejezés vs. típusos kifejezés A probléma formálisan leírt megoldása (program)
Típusos kifejezések • Alaptípusok: Integer, Boolean, Character. • Típus: < név > = < értékek halmaza > • Boolean
= { true, false }
• Integer
= { ... -1, 0, 1, ... }
• Származtatott típusok (magasabb típusok): n ≥ 1 T1 × ... × Tn → T Argumentum típusok
Érték típus
Argumentumok száma n: a tömb dimenziója
Változó, konstans, reláció, függvény • Változók • Egyszerű változók • Tömb változók (Array ) ( • Konstansok • Alaptípusok konstansok • Összetett típusú (magasabb típusú) konstansok • Reláció, függvény • T1 × ... × Tn → T • Ha T értéktípus Boolean, akkor reláció szimbólum, egyébként függvény szimbólum. • Reláció: • Függvény:
≤ : Integer Integer → Boolean [infix]; + : Integer Integer → Integer [infix];
Tömb típus • Az Integer → T típusú α tömb esetében α egy olyan függvényt jelöl, amely Integer értékek halmazáról képez a T által jelölt értékek halmazára. • Ha k ≤ l, akkor α [ k : l ] jelölés az intervallumot { i | k ≤ i ≤ l }-re korlátozza • Ha t ∈ T; i ∈ Integer, akkor pl.: t = α [ i ] Ha az α tömb típusa
Integer × Boolean → Boolean és i ∈ Integer; B ∈ Boolean,
akkor pl.
α( i, B )
B‘ ∈ Boolean esetén pl.:
B' ← α( i, B ) egy értékadás.
egy Bool kifejezés,
Tömb típus
• Adott egy T1 × ... × Tn → T típus-szimbólum… • Példa: Egy tömb leképezés típus-szimbóluma • Integer × Boolean → Boolean • A ∈ Array, k ∈ Integer, B, ok ∈ Boolean esetén • B ∨ A[ k+1, ok ] • A[ 2 × k, ¬ok ]
bool kifejezés, bool kifejezés.
Típusos kifejezés rekurzív definíciója • T típus egy egyszerű változója egy T típusú kifejezés. • T típus egy egyszerű konstansa egy T típusú kifejezés. • Ha s1, ..., sn rendre T1, ..., Tn típusú kifejezések, és op egy konstans a T1 × ... × Tn → T típusból, akkor op( s1, ..., sn ) egy T típusú kifejezés. • Ha s1, ..., sn rendre T1, ..., Tn típusú kifejezések, és α egy tömb a T1 × ... × Tn → T típusból, akkor α [ s1, ..., sn ] egy T típusú kifejezés. • Ha B egy Boolean típusú kifejezés, továbbá s1 és s2 T típusú kifejezések, akkor if B then s1 else s2 fi egy T típusú kifejezés.
Kifejezések felírási formái • Infix forma: s1 op s2 • Példa • + : Integer Integer → Integer [infix], valamint • i, j, k ∈ Integer esetén
k=i+j
• Prefix forma: op( s1, s2 ) vagy op( s ) • Példa • add: Integer Integer → Integer, valamint • i, j, k ∈ Integer esetén k = add( i, j ) • Példa • ¬ : Boolean → Boolean • i, k ∈ Boolean esetén k = ¬ i
Kifejezések felírási formái • Post fix forma: s op • Például: Faktoriális • ! : nat → nat [postfix] • n, k ∈ nat • n = k! • Kifejezés forma: • Például: vektor, amelynek elemei Integer értékek • Vektor műveletek: • _ [ _ ] : vector nat → Integer • v ∈ vector, k ∈ nat, i ∈ Integer • i=v[k]
Kifejezések kiértékelése
• Zárójelezések elkerülése a műveletek prioritási sorrendje alapján 1. 2. 3. 4. 5.
szorzás × , osztás /, moduló összeadás +, kivonás =, <, ≤, >, ≥ ∨, ∧ ⇒, ⇔
• Például: • x + y mod(n) értelmezése: •p∧q⇒r értelmezése:
x + (y mod(n)) (p ∧ q) ⇒ r
