Patikimų programų sudarymo metodai


Informatikos konspektas. Literatūra. Įvadas. Formalūs metodai. Kas yra formalūs metodai? Formalios sistemos. Formalios kalbos. Semantika. Išvedimo sistemos. Įrodymai ir teoremos. Išvedamumas. Programinės įrangos inžinierijos kontekstas. Formalūs metodai programinės įrangos inžinierijoje. Formalių metodų panaudojimas programavimo inžinierijoje. Formalių metodų taikymo lygmenys. Skaičiavimo modeliai, vartojami specifikacijoje. Specifikacijos paradigmos ir apimtis. Neformalus įvadas į logiką ir aibių teoriją. Aibės. Teiginiai ir predikatai. Plačiau apie aibes. Pirmoji specifikacija. Neformalus pristatymas. Formalesnis pristatymas. Z tipų sistema. Žymėjimo išplėtimas. Keletas specifikacijų kūrimo vienetų. Įvestų žymėjimų santrauka. Ryšiai. Funkcijos. Operacijos su funkcijomis. Sekos. Z kalbos žymėjimas: schemos ir specifikacijų struktūros. Pirmos specifikacijos pertvarkymas. Rečiau naudojama teorija. Pavyzdžiai. Formalus pagrindimas. Deklaravimai.


2 pavyzdys. Čia pateikiami keli eilučių pavyzdžiai sudaryti iš bendro alfabeto, naudojamo realiems skaičiams ir knygų dalių numeriams žymėti.

Priimtini dalių numeriai “3.2” “1.2.3” “1” “3.6.1”

Nepriimtini dalių numeriai “.7” “3.”

Priimtini realūs skaičiai “23.7” “12” “12.” “.76” “.7”

Nepriimtini realūs skaičiai “3.6.1”

3 pavyzdys. Kalba L turi alfabetą {*,(}, ir jos sintaksė (išreikšta Lietuvių metakalba) yra pateikta gramatine taisykle:

Šie pavyzdžiai yra L kalbos taisyklės

4 pavyzdys. Tolimesnės taisyklės sukuria esybę, pavadintą digit, kuri gali būti vienas iš simbolių 0...9, ir po to ši esybė panaudojama šešioliktainio skaičiaus esybės aprašyme

5 pavyzdys. Tolimesnės taisyklės aprašo bet kurią eilutę 00, 01 ir iki 99, panaudojant aukščiau aprašytą esybę digit.

6 pavyzdys. Čia pateikiama kalba dešimtainių skaičių be ženklo (unsigned integer) užrašymui. Alfabetas {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, .} ir gramatinės taisyklės

unsigned decimal = unsigned integer | decimal fraction | unsigned integer, decimal fraction;

ir parašius simbolius vieną šalia kito, reiškia, kad jų reikšmės turi būti sudėtos. Pavyzdžiui,

ir parašius simbolius vieną šalia kito, reiškia, kad jų reikšmės turi būti sudėtos, t.y. I2(xy)=I2(x)+I2(y). Dabar

9 pavyzdys. Čia pateikta paprasta formali sistema. Kalbos alfabetas yra {*, (, (} ir sintaksė pateikta gramatinėmis taisyklėmis

10 pavyzdys. Norint parodyti, kad *(****(***** yra tiesiogiai išvesta iš taisyklės *(***(****, 9 pavyzdžio formalioje sistemoje, reikia nustatyti a, b ir c.

X(Y = {(1, p), (1, q), (1, r), (2, p), (2, q), (2, r)}

Tarkim, kad ( ir g abi yra tipo X  Y funkcijos su šaltiniu X ir tikslu Y. Tada:

Kad būtų tenkinamas Library’Predicate, #(issued’ ({r?}) reikšmė turi būti nedidesnė nei maxloans, tačiau prie (issued ({r?}) yra pridedamas naujas elementas, taigi:

Tarkime, kad B, B1, B2, ... yra pakuotės su elementais iš aibės X; t, t1, t2, ..., tn yra tipo X išraiškos; x, x1, x2, ..., xn – kintamieji; ir n, k1, k2, ...kn – sviekieji skaičiai.

[t1, t2, ..., tn]Pakuotė, sudaryta iš t1, t2, ..., tn elementų su dažnumu, kuriuo jie pasirodo šiame sąraše.

bagof BPakuotė, sudaryta iš aibės S, įtraukiant visus aibės S elementus su dažniu, lygiu 1.

pilnoji tvarka:dalinė tvarka, turinti papildomą savybę:(x,y:X((x(y) ( hbr ( (y(x) ( hbr

Vadinasi ( yra dalinė tvarka. Kadangi visiems x, y(Z x(y arba y(x, gauname, kad ( yra pilna tvarka.

NonDecreasing == {s : seq X | ( i, j : dom s ( (i

Ne visi vagonai gali dirbti bet kuriuo momentu. Vagonas gali būti remontuojamas, arba, pavyzdžiui, naujas vagonas gali būti bandomas, prieš jį išnuomojant.

Vagonas išnuomojamas, klientui užsisakius. Užsakymai yra išankstiniai. Pateikiant užsakymą, reikia sumokėti minimalų užstatą. Atėjus nuomos laikui, vagonus iš garažo pasiima klientas, o nuomos sutarties pabaigoje juos ten patys grąžina.

(vc: VanClass ( (d: Date ( -- o#{b: dom commit | commit(b)=vc ( d fallsIn hirePeriods(b)}( #{v: dom fleet | fleet(v) = vc}

4.Parodysime, kad iš p ( r ( q galime išvesti p ( q. Kai įrodysime tai,

Taigi, (x:N ( (y:N ( y>x yra ekvivalentus (m:N ( (n:N( n>m.

Kada du kvantoriai yra greta, kartais galima pakeisti jų eiliškumą. Šios taisyklės rodo, kada tai saugu daryti:

Pavyzdžiui, pasakymas, kad n ( {x : Even | x > 8} yra ekvivalentus pasakymui n( Even(n > 8.

( ( { f:S  T| (x,y: dom f ( f x = f y ( x=y}

dom out = dom(in;ref;symtab)(dom(in;num)(dom(in;op;mnem) [1,S5,S6]

Yra du pagrindiniai reikalavimai, kurie bus pateikti 2 skirtingais būdais: jei sakome, kad S detalizuoja R, tai užrašome: R(S, jei:

Rel1 ir Rel2 ryšių atveju, kai abiejų tipai X ( Y, mes sakome, kad Rel2 detalizuoja Rel1, užrašoma Rel1(Rel2, kai dvi tokios savybės, atitinkančios Tinkamumo ir Teisingumo kriterijus galioja:

Tarkime mes norime parodyti, kad ChooseSmaller ( AlwaysOne. Tuomet reikalavimas pre ChooseSmaller  pre AlwaysOne prilygsta :

Patikimų programų sudarymo metodai. (2010 m. Kovo 03 d.). http://www.mokslobaze.lt/patikimu-programu-sudarymo-metodai.html Peržiūrėta 2016 m. Gruodžio 09 d. 02:03