Исправност (рачунарство)
Утеоријском рачунарству,алгоритамјеисправану односу на спецификацију ако се понаша онако како је дефинисано. Најбоље истражена јефункционалнаисправност, која се односи на улазно-излазно понашање алгоритма: за сваки улаз он производи излаз који задовољава спецификацију.[1]
У оквиру овог другог појма,делимична исправност,која захтева да ће одговор бити тачан,акосе врати, разликује се одпотпуне тачности,која додатно захтева да се одговор на крају врати, односно да се алгоритам прекида. Сходно томе, да би седоказалапотпуна исправност програма, довољно је доказати његову делимичну исправност и његов завршетак.[2]Последња врста доказа (доказ прекида) никада не може бити потпуно аутоматизована, јерпроблем заустављањајенеодлучив.
| Делимично исправанЦпрограм за проналажење најмањег непарног савршеног броај, његова потпуна исправност је непозната од 2023. године. |
// враћа збир правих делилаца броја н
staticintdivisorSum(intn){
inti,sum=0;
for(i=1;i<n;++i)
if(n%i==0)
sum+=i;
returnsum;
}
// враћа најмањи непарни савршени број
intleastPerfectNumber(void){
intn;
for(n=1;;n+=2)
if(n==divisorSum(n))
returnn;
}
|
На пример, ако претражујемо редомцеле бројеве1, 2, 3,… како бисмо пронашли неки феномен—рецимо непарансавршен број—лакo је написати програм који је делимично исправан. Међутим, тврдити да је овај програм потпуно исправан значило би тврдити нешто што тренутно није познато утеорији бројева.
Доказ би морао бити математички доказ, под претпоставком да су и алгоритам и спецификација дати формално. Нарочито се не очекује да то буде тврдња о исправности за дати програм који имплементира алгоритам на датој машини. То би укључивало таква разматрања као што су ограничењарачунарске меморије.
Један резултат у теорији доказа, познат каоКари-Хауардова кореспонденција,наводи да доказ функционалне исправности у конструктивној логици одговара одређеном програму уламбда рачуну.Претварање доказа на овај начин назива сеекстракција програма.
Хорова логика(енг.Hoare logic) је специфичанформални системза ригорозно расуђивање о исправности рачунарских програма.[3]Користи аксиоматске технике за дефинисање семантике програмских језика и аргументовање о исправности програма путем тврдњи познатих као Хорове тројке.
Тестирање софтвераје свака активност која има за циљ процену атрибута или способности програма или система и утврђивање да ли испуњава тражене резултате. Иако је од кључног значаја за квалитет софтвера и широко коришћено од стране програмера и тестера, тестирање софтвера и даље остаје уметност, због ограниченог разумевања принципа софтвера. Тешкоћа у тестирању софтвера произилази из сложености софтвера: не можемо у потпуности тестирати програм умерене сложености. Тестирање обухвата више од само отклањања грешака. Сврха тестирања може бити осигурање квалитета, верификација и валидација или процена поузданости. Тестирање се може користити и као генерички показатељ. Тестирање исправности и тестирање поузданости су две главне области тестирања. Тестирање софтвера је компромис између буџета, времена и квалитета.[4]
Види такође
[уреди|уреди извор]Референце
[уреди|уреди извор]- ^Dunlop, Douglas D.;Basili, Victor R.(јун 1982).„A Comparative Analysis of Functional Correctness”.Communications of the ACM.14(2): 229–244.doi:10.1145/356876.356881.
- ^Manna, Zohar; Pnueli, Amir (1974).„Axiomatic approach to total correctness of programs”.Acta Informatica(на језику: енглески).3(3): 243—263.ISSN0001-5903.doi:10.1007/BF00288637.
- ^Hoare, C. A. R.„An axiomatic basis for computer programming”.Communications of the ACM(на језику: енглески).12(10): 576—580.ISSN0001-0782.doi:10.1145/363235.363259.
- ^Pan, Jiantao (пролеће 1999).„Software Testing”(coursework). Carnegie Mellon University.Приступљено21. 11. 2017.
Литература
[уреди|уреди извор]- "Human Language Technology. Challenges for Computer Science and Linguistics."Google Books. N.p., n.d. Web. 10 April 2017.
- "Security in Computing and Communications."Google Books. N.p., n.d. Web. 10 April 2017.
- "The Halting Problem of Alan Turing - A Most Merry and Illustrated Explanation."The Halting Problem of Alan Turing - A Most Merry and Illustrated Explanation. N.p., n.d. Web. 10 April 2017.
- Turner, Raymond, and Nicola Angius. "The Philosophy of Computer Science."Stanford Encyclopedia of Philosophy.Stanford University, 20 August 2013. Web. 10 April 2017.
- Dijkstra, E. W. "Program Correctness". U of Texas at Austin, Departments of Mathematics and Computer Sciences, Automatic Theorem Proving Project, 1970. Web.