416:
principles of software. The difficulty in software testing stems from the complexity of software: we can not completely test a program with moderate complexity. Testing is more than just debugging. The purpose of testing can be quality assurance, verification and validation, or reliability estimation. Testing can be used as a generic metric as well. Correctness testing and reliability testing are two major areas of testing. Software testing is a trade-off between budget, time and quality.
906:
913:
366:
A proof would have to be a mathematical proof, assuming both the algorithm and specification are given formally. In particular it is not expected to be a correctness assertion for a given program implementing the algorithm on a given machine. That would involve such considerations as limitations on
415:
is any activity aimed at evaluating an attribute or capability of a program or system and determining that it meets its required results. Although crucial to software quality and widely deployed by programmers and testers, software testing still remains an art, due to limited understanding of the
408:
for reasoning rigorously about the correctness of computer programs. It uses axiomatic techniques to define programming language semantics and argue about the correctness of programs through assertions known as Hoare triples.
674:
Dijkstra, E. W. "Program
Correctness". U of Texas at Austin, Departments of Mathematics and Computer Sciences, Automatic Theorem Proving Project, 1970. Web.
556:
355:—it is quite easy to write a partially correct program (see box). But to say this program is totally correct would be to assert something
50:
correctness, which refers to the input-output behavior of the algorithm: for each input it produces an output satisfying the specification.
699:
73:
a program's total correctness, it is sufficient to prove its partial correctness, and its termination. The latter kind of proof (
942:
937:
754:
916:
865:
17:
383:
860:
660:." The Halting Problem of Alan Turing - A Most Merry and Illustrated Explanation. N.p., n.d. Web. 10 April 2017.
692:
830:
825:
657:
31:
881:
779:
599:
891:
734:
947:
739:
685:
564:
480:
578:
515:
Manna, Zohar; Pnueli, Amir (September 1974). "Axiomatic approach to total correctness of programs".
886:
664:
650:
643:
356:
92:
800:
835:
820:
815:
573:
43:
764:
744:
445:
8:
425:
82:
591:
534:
497:
450:
430:
387:
70:
617:
769:
595:
74:
501:
708:
583:
538:
526:
517:
489:
435:
412:
729:
391:
368:
78:
351:
1, 2, 3, … to see if we can find an example of some phenomenon—say an odd
774:
440:
352:
475:
931:
658:
The
Halting Problem of Alan Turing - A Most Merry and Illustrated Explanation
471:
405:
360:
855:
805:
552:
379:
644:
Human
Language Technology. Challenges for Computer Science and Linguistics
587:
493:
759:
749:
401:
375:
69:
eventually returned, i.e. the algorithm terminates. Correspondingly, to
530:
795:
35:
27:
Quality of an algorithm being correct with respect to a specification
677:
348:
61:
an answer is returned it will be correct, is distinguished from
671:. Stanford University, 20 August 2013. Web. 10 April 2017.
386:, states that a proof of functional correctness in
476:"A Comparative Analysis of Functional Correctness"
929:
653:." Google Books. N.p., n.d. Web. 10 April 2017.
646:." Google Books. N.p., n.d. Web. 10 April 2017.
508:
693:
557:"An axiomatic basis for computer programming"
65:, which additionally requires that an answer
46:if it behaves as specified. Best explored is
469:
347:For example, successively searching through
99:its total correctness is unknown as of 2023
514:
394:. Converting a proof in this way is called
700:
686:
77:) can never be fully automated, since the
577:
463:
107:// return the sum of proper divisors of n
651:Security in Computing and Communications
620:(coursework). Carnegie Mellon University
390:corresponds to a certain program in the
14:
930:
242:// return the least odd perfect number
681:
663:Turner, Raymond, and Nicola Angius. "
551:
912:
707:
545:
669:Stanford Encyclopedia of Philosophy
615:
24:
665:The Philosophy of Computer Science
25:
959:
866:List of system quality attributes
911:
905:
904:
609:
13:
1:
636:
97:the least odd perfect number,
943:Theoretical computer science
616:Pan, Jiantao (Spring 1999).
32:theoretical computer science
7:
882:Software quality management
861:Non-functional requirements
419:
384:Curry–Howard correspondence
10:
964:
938:Formal methods terminology
892:Software quality assurance
53:Within the latter notion,
900:
874:
848:
788:
722:
715:
565:Communications of the ACM
481:Communications of the ACM
887:Software quality control
456:
104:
588:10.1145/363235.363259
494:10.1145/356876.356881
470:Dunlop, Douglas D.;
446:Compiler correctness
849:Standards and lists
426:Formal verification
357:currently not known
55:partial correctness
618:"Software Testing"
531:10.1007/BF00288637
451:Program derivation
431:Design by contract
396:program extraction
388:constructive logic
248:leastPerfectNumber
91:Partially correct
42:with respect to a
925:
924:
844:
843:
770:Understandability
472:Basili, Victor R.
345:
344:
75:termination proof
63:total correctness
57:, requiring that
18:Total correctness
16:(Redirected from
955:
948:Software quality
915:
914:
908:
907:
720:
719:
709:Software quality
702:
695:
688:
679:
678:
630:
629:
627:
625:
613:
607:
606:
605:on 4 March 2016.
604:
598:. Archived from
581:
561:
555:(October 1969).
549:
543:
542:
518:Acta Informatica
512:
506:
505:
467:
436:Program analysis
413:Software testing
339:
336:
333:
330:
327:
324:
321:
318:
315:
312:
309:
306:
303:
300:
297:
294:
291:
288:
285:
282:
279:
276:
273:
270:
267:
264:
261:
258:
255:
252:
249:
246:
243:
240:
237:
234:
231:
228:
225:
222:
219:
216:
213:
210:
207:
204:
201:
198:
195:
192:
189:
186:
183:
180:
177:
174:
171:
168:
165:
162:
159:
156:
153:
150:
147:
144:
141:
138:
135:
132:
129:
126:
123:
120:
117:
114:
111:
108:
88:
87:
21:
963:
962:
958:
957:
956:
954:
953:
952:
928:
927:
926:
921:
896:
870:
840:
784:
735:Maintainability
711:
706:
639:
634:
633:
623:
621:
614:
610:
602:
579:10.1.1.116.2392
572:(10): 576–580.
559:
553:Hoare, C. A. R.
550:
546:
513:
509:
468:
464:
459:
422:
392:lambda calculus
369:computer memory
341:
340:
337:
334:
331:
328:
325:
322:
319:
316:
313:
310:
307:
304:
301:
298:
295:
292:
289:
286:
283:
280:
277:
274:
271:
268:
265:
262:
259:
256:
253:
250:
247:
244:
241:
238:
235:
232:
229:
226:
223:
220:
217:
214:
211:
208:
205:
202:
199:
196:
193:
190:
187:
184:
181:
178:
175:
172:
169:
166:
163:
160:
157:
154:
151:
148:
145:
142:
139:
136:
133:
130:
127:
124:
121:
118:
115:
112:
109:
106:
98:
96:
95:program to find
79:halting problem
28:
23:
22:
15:
12:
11:
5:
961:
951:
950:
945:
940:
923:
922:
920:
919:
909:
901:
898:
897:
895:
894:
889:
884:
878:
876:
872:
871:
869:
868:
863:
858:
852:
850:
846:
845:
842:
841:
839:
838:
833:
828:
823:
818:
813:
808:
803:
798:
792:
790:
786:
785:
783:
782:
777:
775:Loose coupling
772:
767:
762:
757:
752:
747:
742:
737:
732:
726:
724:
717:
713:
712:
705:
704:
697:
690:
682:
676:
675:
672:
661:
654:
647:
638:
635:
632:
631:
608:
544:
525:(3): 243–263.
507:
488:(2): 229–244.
461:
460:
458:
455:
454:
453:
448:
443:
441:Model checking
438:
433:
428:
421:
418:
404:is a specific
353:perfect number
343:
342:
105:
101:
100:
26:
9:
6:
4:
3:
2:
960:
949:
946:
944:
941:
939:
936:
935:
933:
918:
910:
903:
902:
899:
893:
890:
888:
885:
883:
880:
879:
877:
873:
867:
864:
862:
859:
857:
854:
853:
851:
847:
837:
834:
832:
829:
827:
824:
822:
819:
817:
814:
812:
809:
807:
804:
802:
799:
797:
794:
793:
791:
787:
781:
780:Orthogonality
778:
776:
773:
771:
768:
766:
763:
761:
758:
756:
753:
751:
748:
746:
743:
741:
738:
736:
733:
731:
728:
727:
725:
721:
718:
714:
710:
703:
698:
696:
691:
689:
684:
683:
680:
673:
670:
666:
662:
659:
655:
652:
648:
645:
641:
640:
619:
612:
601:
597:
593:
589:
585:
580:
575:
571:
567:
566:
558:
554:
548:
540:
536:
532:
528:
524:
520:
519:
511:
503:
499:
495:
491:
487:
483:
482:
477:
474:(June 1982).
473:
466:
462:
452:
449:
447:
444:
442:
439:
437:
434:
432:
429:
427:
424:
423:
417:
414:
410:
407:
406:formal system
403:
399:
397:
393:
389:
385:
381:
377:
372:
370:
364:
362:
361:number theory
358:
354:
350:
103:
102:
94:
90:
89:
86:
84:
80:
76:
72:
68:
64:
60:
56:
51:
49:
45:
44:specification
41:
37:
33:
19:
856:ISO/IEC 9126
810:
806:Adaptability
668:
622:. Retrieved
611:
600:the original
569:
563:
547:
522:
516:
510:
485:
479:
465:
411:
400:
395:
380:proof theory
373:
365:
346:
66:
62:
58:
54:
52:
47:
39:
29:
811:Correctness
801:Reliability
765:Testability
760:Scalability
755:Readability
750:Reusability
745:Portability
740:Flexibility
624:21 November
402:Hoare logic
376:deep result
83:undecidable
932:Categories
826:Robustness
821:Efficiency
637:References
317:divisorSum
116:divisorSum
48:functional
875:Processes
796:Usability
716:Qualities
596:207726175
574:CiteSeerX
36:algorithm
831:Security
816:Accuracy
789:External
723:Internal
502:18627112
420:See also
349:integers
917:Commons
539:2988073
40:correct
836:Safety
594:
576:
537:
500:
382:, the
329:return
230:return
110:static
603:(PDF)
592:S2CID
560:(PDF)
535:S2CID
498:S2CID
457:Notes
71:prove
34:, an
730:Size
626:2017
254:void
176:<
667:."
584:doi
527:doi
490:doi
378:in
359:in
272:for
263:int
245:int
233:sum
218:sum
155:for
143:sum
134:int
122:int
113:int
81:is
38:is
30:In
934::
590:.
582:.
570:12
568:.
562:.
533:.
521:.
496:.
486:14
484:.
478:.
398:.
374:A
371:.
363:.
326:))
314:==
305:if
296:+=
221:+=
209:==
194:if
185:++
85:.
67:is
59:if
701:e
694:t
687:v
656:"
649:"
642:"
628:.
586::
541:.
529::
523:3
504:.
492::
338:}
335:;
332:n
323:n
320:(
311:n
308:(
302:)
299:2
293:n
290:;
287:;
284:1
281:=
278:n
275:(
269:;
266:n
260:{
257:)
251:(
239:}
236:;
227:;
224:i
215:)
212:0
206:i
203:%
200:n
197:(
191:)
188:i
182:;
179:n
173:i
170:;
167:1
164:=
161:i
158:(
152:;
149:0
146:=
140:,
137:i
131:{
128:)
125:n
119:(
93:C
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.