Formali specifikacija

Straipsnis iš Vikipedijos, laisvosios enciklopedijos.
Peršokti į: navigaciją, paiešką
 Broom icon.svg  Šį puslapį ar jo dalį reikia sutvarkyti pagal Vikipedijos standartus.
Jei galite, sutvarkykite; apie sutvarkymą galite pranešti specialiame Vikipedijos projekte.
 NoFonti.svg  Šiam straipsniui ar jo daliai trūksta šaltinių ar nuorodų į juos.
Jūs galite padėti Vikipedijai įrašydami tinkamas išnašas ar nuorodas į šaltinius.

Informatikoje formali specifikacija yra programinės įrangos ar techninės įrangos aprašymas, kuris gali būti naudojama analizei ir įgyvendinimui. Dažniausiai specifikacijoje nurodoma, ką sistema privalo atlikti, o ne kaip tai turi būti atliekama. Turint tokią specifikaciją, formalus verifikavimas leidžia patikrinti, ar planuojama realizacija atitinka reikalavimus. Tai leidžia aptikti sistemos projektavimo klaidas bei ankstyvoje programinės ar techninės įrangos kūrimo fazėje, dar prieš įgyvendinant sistemą. Tai turi privalumą, kadangi netinkami kūriamos sistemos projektai gali būti tikslinami iki sistemos įgyvendinimo. Taip pat galima transformuoti naudojant laipsniško tobulinimo metodiką, įrodant arba patikrinant kiekvieno tobulinimo žingsnio teisingumo, ir taip gaunant sistemą, kurios teisingumas yra įrodytas.

Projektas (ar realizacija) negali būti „teisingi kalbant“ atsietai, bet gali būti „teisingas atsižvelgiant į specifikaciją“. Šiuo atveju neanalizuojama, ar formali specifikacija atitinka užduoti, tai sprendžiama atskirai. Tai irgi sudėtinga problema, kadangi ji suvedama į abstrakčią formalią neformalios konkrečios probleminės srities aprašymo užduotį, kuri negali būti formalizuota. Tačiau įmanoma validuoti specifikaciją įrodant teoremas su savybėmis kurias specifikacija aprašo. Jei teoremos teisingos, jos pagerina specifikuotojo supratimą apie specifikacijas ir jų ryšį su problemos sritimi. Jeigu ne, specifikacija greičiausiai turi būti pakeista taip, kad geriau atspindėtų probleminę sritį arba būtų geriau išnaudojamos taikomo specifikavimo metodo galimybės.

Z notacija vienas iš labiausiai žinomų formalių specifikavimo kalbų pavyzdžių. Kitos yra Vienos Plėtojimo Metodo Specifikacijos kalba ir B-metodo Abstrakto mechanizmo kalba.

Taip pat skaitykite[taisyti | redaguoti kodą]

Nuorodos[taisyti | redaguoti kodą]