Formaalsed meetodid

From mmmv_kos
Jump to: navigation, search


Staatiline testimine seisneb testi definitsioonis olevatele küsimustele vastuste otsimises objekti vaatlemise kaudu, ilma, et vaadeldavat objekti testimise käigus mõjutataks. Illustratsioon: maja seinas oleva prao fotografeerimine, programmikoodist programmikoodi töö käigus toimuva järeldamine. Formaalsete meetodid on mõeldud staatilise testimise automatiseerimiseks.


Staatilise testimise üldskeem:


järeldatud_piirangud=func_teoreemitõestajad_ja_muu_infrastruktuur(testijate_defineeritud_piirangud)


piirangute_hulk_2=unique(testijate_defineeritud_piirangud+järeldatud_piirangud)


testiaruanded_mis_kirjeldavad_kuidas_uuritav_objekt_ei_mahu_piirangute_poolt_seatud_piiridesse = =func_objekti_omaduste_uurimine(uuritav_objekt,piirangute_hulk_2)


Järgnev tekst käsitleb vaid tarkvaraga ning arvutustehnikaga seonduvat. Staatilise testimise peamine eelis dünaamilise testimise ees seisneb selles, et sellega on vähema testide kirjutamise töö vaevaga võimalik dünaamilisest testimisest rohkem juhtumeid katta, kuid staatiline testimine ei asenda dünaamilist testimist, sest staatilisel testimisel kasutatav piirangute hulk ei pruugi olla kõiki juhtumeid hõlmav. Sarnaselt dünaamilisele testimisele on staatilisel testimisel väga palju erinevaid vorme, alamvaldkondi, nimetusi: "theorem proving", "model verification", "static analysis", jne.


Vähemalt osade programmeerimiskeelte korral eksisteerib kõigi antud programmeerimiskeeles kirjutatud programmidele ühine piirangute hulk, mida aja jooksul, targemaks saades, täiendatakse. Näiteks C korral sisaldab see piirangute hulk tingimusi, et üle massiivi ääre ei kirjutata/loeta, ning, et int ja struct tüüpi muutujatele ei ole defineeritud vaikimisi operaatorit "+".


Mõnikord loetakse osa koodi piirangute kirjeldusi koodi osaks olevatest kommentaaridest, nagu seda SPARK'i korral eeltingimuste(preconditions) ja järeltingimuste(post-conditions) korral tehakse. Mõnikord kasutatakse skeemi, kus programmikoodi asemel joonistatakse mõne spetsiaaltööriistaga mingi diagramm, "mudel", mille kohta defineeritakse piirangud ning siis, võimaluse korral, transleeritakse too skeem mõnda sellisesse programmeerimiskeelde, mida arendatava tarkvara alamosana tööle saab lasta. Mõnikord kirjeldatakse "mudel" mõnes spetsiaalselt piirangute kehtivuse kontrolli lihtsuse järgi optimeeritud programmeerimiskeeles, mille kood arenduses oleva tarkvaraga ühilduvasse programmeerimiskeelde transleeritakse.


Viited

Raamatuid ja standardeid


Ajaveebid


Võistlused