Formalūs metodai

Šiam straipsniui ar jo daliai trūksta išnašų į patikimus šaltinius.
Jūs galite padėti Vikipedijai pridėdami tinkamas išnašas su šaltiniais.

Formalūs metodai – logika bei matematika besiremiantys metodai informatikoje ir programų inžinerijoje skirti programinės ir aparatūrinės įrangos specifikavimui, modeliavimui, kūrimui ir verifikavimui. Tikimasi, kad panašiai, kaip ir kitose inžinerijos srityse, formalūs metodai leis kurti patikimesnes ir atsparesnes klaidoms sistemas. Tačiau kadangi jų taikymas yra brangus, tai jie taikomi kuriant padidinto patikimumo sistemas.

Formalūs metodai taiko įvairius teorinės informatikos įrankius, pvz., logiką, formalias kalbas, automatų teoriją, programų semantiką, taip pat tipų teoriją, algebrinius duomenų tipus siekdama išspręsti programinės ir aparatūrinės įrangos specifikavimo ir verifikavimo uždavinius.

Taksonomijos redaguoti

Formalūs metodai naudojami keliais lygiais:

0 Lygis: gali būti pradėtos formalios specifikacijos ir tuomet iš to neformaliai vystoma programa. Tai yra praminta formaliais nesudėtinais/lengvais metodais. Daugeliu atvejų šis metodas gali būti pats rentabiliausias (labiausiai apsimokantis) pasirinkimas.

1 Lygis: formali raida ir formali kontrolė (tikrinimas) gali būti naudojami sukurti programą formalesniu būdu. Pavyzdžiui, iš programos specifikacijų gali būti pradėtos įrodymų savybės arba tobulinimas. Tai labiausiai tinka vientisose (aukšto integralumo) sistemose apimančiose saugumą arba patikimumą.

2 lygis: patikros programos teorema gali būti naudojama pradėti pilnai formaliai mašinų patikrintus įrodymus. Tai gali būti labai brangu ir praktiškai verta, jei klaidų kaina yra ypatingai didelė (pvz.: kritinėse mikroprocesorių dizaino dalyse).

Kas liečia kalbos semantikos programavimą, formalių metodų stiliai apytikriai klasifikuojami į:

Denotacijos (reikšmės) semantika, kur sistemos reikšmė išreiškiama matematine domenų teorija. Tokių metodų propaguotojai pasikliauja gerai perprasta domenų prigimtimi suteikti sistemai prasmę. Kritikai atkreipia dėmesį į tai, kad ne į kiekvieną sistemą gali būti intuityviai ar natūraliai žiūrima kaip į funkciją.

Operacinė (naudojimo) semantika, kur sistemos reikšmė išreiškiama kaip, reikia manyti, paprastesnių kompiuterinio modelio veiksmų seka. Šių metodų propaguotojai atkreipia dėmesį į jų modelių, kaip priemonės išreiškiančios aiškumą, paprastumą. Kritikai atremia kaltinimus, kad semantikos problema buvo ką tik atidėta (kas apibrėžia paprastesnio modelio semantiką?).

Aksiominė semantika, kur sistemos reikšmė išreiškiama prielaidų ir baigties sąlygų kalba, kuri yra teisinga (tiesa) prieš ir po to, kai sistema atitinkama tvarka atlieka užduotį. Propaguotojai pažymi ryšį su klasikine logika. Kritikai pažymi, kad tokia semantika niekada tikrai neapibūdina to, ką sistema daro (tiktai kas yra tiesa prieš ir po to).

Lengvasvoriai formalūs metodai redaguoti

Kai kurie praktikuojantys asmenys mano, kad formalių metodų bendruomenė per daug pabrėžia visišką specifikacijos arba formalizavimą. Jie tvirtina, kad į tai įtrauktų kalbų ekspresyvumas, taip pat kaip modeliuojamų sistemų sudėtingumas, visišką formalizaciją padaro sudėtinga ir brangia užduotimi. Kaip alternatyva (pasirinkimas), buvo pasiūlyti įvairūs lengvasvoriai formalūs metodai, pabrėžiantys dalinę specifikaciją ir kryptingą taikymą. Šių lengvasvorių formalių metodų požiūris į formalius metodus apima lydinio objekto modeliavimo žymėjimą, kai kurių Denn’io Z žymėjimo aspektų su use case varomu plėtojimu/vystymu sintezę ir CSK bei VDM įrankius.

Naudojimas redaguoti

Formalieji metodai gali būti taikomi įvairiose plėtojimo proceso dalyse.

Specifikacijos redaguoti

Formalūs metodai gali būti naudojami apibūdinti bet kuriame lygyje ar lygiuose plėtotiną sistemą. Šis formalus apibūdinimas gali būti naudojamas kaip tolimesnių plėtojimo (vystymo) veiksmų vedlys (žiūrėti sekančias teksto dalis), papildomai, jie gali būti naudojami plėtojamos sistemos reikalavimų patvirtinimui, patvirtinti, kad reikalavimai buvo iki galo ir teisingai nustatyti. Formalios specifikacijos sistemų reikmė pastebėta metų metus. ALGOL 60 ataskaitoje, Džonas Bakus pristatė formalų žymėjimą kalbos sintaksės programavimui apibūdinti (vėliau pavadintą Bakus’o normine forma arba Bakus’o – Naur’o forma), BNF. Bakus taip pat aprašė kalbos semantikos programavimo žymėjimo apibūdinimo poreikį. Atsakaita žadėjo, kad ateityje atsiras toks pat tikslus žymėjimas kaip BNF, tačiau tai neįvyko.

Plėtojimas (vystymas) redaguoti

Sukūrus formalią specifikaciją, galima ją naudoti kaip vedlį kol konkreti programa plėtojama projektavimo procese (pavyzdžiui, paprastai realizuojama programinėje įrangoje, bet taip pat potencialiai ir techninėje įrangoje) pavyzdžiui:

jei formali specifikacija yra operacinėje semantikoje, pastebėtas konkrečios sistemos funkcionavimas gali būti palygintas su specifikacijos funkcionavimu (kuris pats turėtų būti vykdomas arba imituojamas). Papildomai, operacinės specifikacijų komandos gali būti pasiduodančios tiesioginiam vertimui į vykdomą kodą.
Jei formali specifikacija yra aksiominėje semantikoje, specifikacijos prielaidos ir baigties sąlygos gali tapti teiginiais vykdomame kode.

Patikrinimas/kontrolė redaguoti

Išplėtojus formalią specifikaciją, ją galima naudoti kaip pagrindą įrodyti specifikacijos ypatybes (su viltimi, darant išvadas apie išplėtotą sistemą).

Į žmogų nukreiptas įrodymas redaguoti

Kartais motyvacija įrodyti sistemos teisingumą yra ne akivaizdus poreikis užtikrinti sistemos teisingumą, bet noras geriau suprasti sistemą. To pasekoje, kai kurie teisingumo įrodymai gaunami matematinio įrodymo stiliumi: naudojant ranka rašytą arba surinktą klaviatūra kalbą, naudojant nenormalumo lygį, bendrą tokiems įrodymams. „Geras“ įrodymas yra tas, kuris yra įskaitomas ir kurį gali supratsi kiti žmonės skaitytojai.

Tokio požiūrio kritikai teigia, kad dviprasmiškumas būdingas natūraliai kalbai tokiuose įrodymuose leidžia neaptikti klaidų, dažnai subtilios klaidos gali būti žemo lygio smulkmenose, paprastai nepastebėtose tokių įrodymų. Papildomai, darbas tam, kad sukurti geros kokybės įrodymą, reikalauja aukšto lygio matematikos išmanymo ir kompetencijos.

Automatizuotas įrodymas redaguoti

Priešingai, auga susidomėjimas tokių sistemų teisingo įrodymo gavimu naudojant automatizuotus būdus. Automatizuotos technikos dalijamos į dvi bendras kategorijas:

Automatizuotos teoremos įrodymas, kur sistema bando gauti formalų įrodymą iš brūkštelėjimo (praktiškai iš nieko) davus sistemos apibūdinimą, loginių aksiomų grupę ir grupę numatymo taisyklių.
Modelio tikrinimas, kur sistema patvirtina tam tikras ypatybes, nepaliaujamai ieškodama visų įmanomų būsenų, į kurias sistema galėtų „įeiti“ jos vykdymo metu.

Nė viena iš šių technikų neveikia be žmogaus pagalbos. Automatizuotos teoremos įrodymas paprastai reikalauja orientavimo, kaip antai kurios ypatybės yra pakankamai įdomios, kad jas tęsti; modelio kontrolinis įrenginys gali greitai įklimpti į milijono neįdomių būsenų tikrinimą, jei neduotas pakankamai abstraktus modelis.

Praktikuojantys tokias sistemas gičijasi, kad rezultatai yra matematiškai tikresni nei žmogaus gautas (padarytas) įrodymas, kadangi visos nuobodžios smulkmenos buvo algoritmiškai patvirtintos. Mokymai, reikalaujantys naudoti tokias sistemas yra taip pat mažesni negu tie, reikalaujantys gerų matematinių įrodymų taip padarydami šias technikas prieinamas platesnei vartotojų įvairovei.

Kritikai pastebi, kad kai kurios iš šių sistemų yra kaip pranašai: ji epaskelbia tiesą, bet jos nepaaiškina. Taip pat yra ir tikrintuvo patvirtinimo problema. Jei programa, padedanti tikrinime, pati yra nepatvirtinta, atsiranda priežastis abejoti gautų rezultatų tikrumu. Kai kurie modernūs modelio tikrinimo įrankiai sukuria „įrodymo protokolą“, detalizuodami kiekvieną įrodymo žingsnį, įgalindami (programą?) jį atlikti duotais įrankiais, nepriklausomu patvirtinimu.

Kritikos redaguoti

Formalių metodų sritis turi savo kritikus. Gauti ranka rašytus teisingumo įrodymus su paslaugų priemonėmis, kitokiomis nei užtikrinančiomis teisingumą, reikia daug laiko ir pinigų. Tai formalius metodus greičiau padaro naudotinus srityse, kur įmanoma atlikti automatizuotus įrodymus naudojant programinę įrangą arba tais atvejais, kai pažeidimo kaina yra didelė. Pavyzdžiui: geležinkelių inžinerijoje ir aerokosminėje inžinerijoje neaptiktos klaidos gali sukelti mirtį, taigi formalūs metodai populiaresni šioje srityje nei kitose taikymo srityse.