Formali specifikacija
| Vaizdas:Broom icon.svg | Šį puslapį ar jo dalį reikia sutvarkyti pagal Enciklopedijos standartus. Jei galite, sutvarkykite; apie sutvarkymą galite pranešti specialiame Enciklopedijos projekte. |
~
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
- Formalūs metodai
- Formalus verifikavimas
- Modelių tikrinimas
- Procesų algebra
- Programų inžinerija
- Z notacija
Nuorodos
- A Case for Formal Specification (Technology) by Coryoth 2005-07-30
- Formal Specification
| ||||||