Tõestamise tasemed Idee- luuakse loogiline arvutus. Selle arvutuse terminites kirjeldatakse spetsifikatsioon ning programm. Tõestatakse, et lähtudes antud sisenditest ja kasutades antud programmi jõutakse nõutud väljunditeni. Ajalugu- tekkis 1960. Avaldati arvukalt töid, kus tõestati lihtsamaid programme. 1990 algas uus tõus, sest oli tekkinud tõestamist teostav tarkvara. Eeltingimused- spetsifikatsioon, programm, loogikavahendid. Eelised- suurem töökindlus. Puudused- töömahukas. Tulemused- programm tõestatakse spetsifikatsiooni suhtes. Tõestamise tasemed- spetsifikatsioon, projekt, programmi kood, tõestusmeetodid, objektkood, täitmine. 37. Cleanroom development: suhe formaalsete meetoditega, testimise korraldus, ülevaade Suhe meetoditega- kasutatakse testimist juhuslike andmetega, statistilist analüüsi, koodi tõestamist. 38
Lühikokkuvõte tõestamisest: · Siht. Näidata, et programm vastab spetsifikatsioonile · Idee. Luuakse loogiline arvutus (valemid, aksioomid, tuletusreeglid, tõestused, teoreemid). Selle arvutuse terminites kujutatakse spetsifikatsiooni (sisendid ja väljundid) ning programmi. Tõestatakse, et lähtudes antud sisenditest ja kasutades antud programmi jõutakse nõutud väljunditeni (tavaliselt ka, et programm lõpetab töö) · Eeltingimused. Spetsifikatsioon, programm, loogikavahendid, vajadus, ressursid, soovitavalt toetav tarkvara · Eelised. Suurem töökindlus, formaalne korrektsus, ainuke viis tsüklite korrektsuse formaalseks põhjendamiseks · Puudused. Töömahukas, sobib halvasti suurte süsteemide jaoks, ei välista spetsifikatsiooni vigu (samuti arenduskeskkonna ja muid vigu), tsükleid on tehniliselt raske tõestada · Tulemused. Programm tõestatakse spetsifikatsiooni suhtes · Suhe teistesse. Kasutatakse koos teiste meetoditega · Hinnang
Jne jne: baasväidete hulk ei saa kunagi kõigi õigete aritmeetikateoreemide tuletamiseks piisavalt suureks. Kui juba aritmeetikat ei saa lõpliku hulga baasväidete abil aksiomatiseerida, siis loomulikult ei saa seda teha ka enamike teiste matemaatikaharude jaoks. Samuti ei saa aksiomatiseerida paljusid muid, matemaatikast täiesti erinevaid mõtlemisvaldkondi, mis tegelevad lõpmatute struktuuridega. See ei tähenda samas, et loogikavahendid oleksid aritmeetika või muude keerulisemate valdkondade juures kasutud: reeglina piisab meile huvi pakkuvate väidete tõestamiseks siiski suhteliselt väikesest hulgast harilikest elementaaraksioomidest. Juhud, kus neist ei piisa, on küll olemas, kuid praktikas väga haruldased. Loogikateaduse uurimisvaldkonnaks ei ole mitte niivõrd keeruliste loogiliste tuletuste mehaaniline sooritamine, kui mõtlemise fundamentaalsete meetodite ja piiride uurimine
annaabi.ee 
