Исправност (рачунарство)
У теоријском рачунарству, алгоритам је исправан у односу на спецификацију ако се понаша онако како је дефинисано. Најбоље истражена је функционална исправност, која се односи на улазно-излазно понашање алгоритма: за сваки улаз он производи излаз који задовољава спецификацију. [1]
У оквиру овог другог појма, делимична исправност, која захтева да ће одговор бити тачан, ако се врати, разликује се од потпуне тачности, која додатно захтева да се одговор на крају врати, односно да се алгоритам прекида. Сходно томе, да би се доказала потпуна исправност програма, довољно је доказати његову делимичну исправност и његов завршетак.[2] Последња врста доказа (доказ прекида) никада не може бити потпуно аутоматизована, јер проблем заустављања је неодлучив.
| Делимично исправан Ц програм за проналажење најмањег непарног савршеног броај, његова потпуна исправност је непозната од 2023. године. |
// враћа збир правих делилаца броја н
static int divisorSum(int n) {
int i, sum = 0;
for (i=1; i<n; ++i)
if (n % i == 0)
sum += i;
return sum;
}
// враћа најмањи непарни савршени број
int leastPerfectNumber(void) {
int n;
for (n=1; ; n+=2)
if (n == divisorSum(n))
return n;
}
|
На пример, ако претражујемо редом целе бројеве 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. ISSN 0001-5903. doi:10.1007/BF00288637.
- ^ Hoare, C. A. R. „An axiomatic basis for computer programming”. Communications of the ACM (на језику: енглески). 12 (10): 576—580. ISSN 0001-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.