정확성(컴퓨터 과학)

Correctness (computer science)

이론 컴퓨터 과학에서 알고리즘은 지정된 대로 동작하는 경우 사양에 대해 정확합니다.가장 잘 탐색되는 것은 알고리즘의 입출력 동작을 나타내는 기능적 정확성입니다(즉,[1] 각 입력에 대해 사양을 충족하는 출력을 생성합니다).

후자의 개념에서, 응답이 반환될 경우 정확해야 하는 부분적 정확성은 완전한 정확성과 구별되며, 이는 추가로 응답이 반환되어야 하는 경우, 즉 알고리즘이 종료된다.이에 대응하여 프로그램의 완전한 정확성을 증명하기 위해서는 프로그램의 부분적 정확성과 [2]종료성을 증명하는 것으로 충분하다.정지 문제는 판별할 수 없기 때문에 후자의 증명(종료 증명)은 완전히 자동화될 수 없습니다.

찾을 C 프로그램을 부분적으로 수정
가장 홀수가 적은 숫자,
2021년 현재 그것의 완전한 정확성은 알려져 있지 않다
// n의 적절한 제수의 합계를 반환합니다. 정적인 인트 제수합(인트 n) {    인트 i, 합 = 0;    위해서 (i=1; i< >n; ++i)       한다면 (n % i == 0)          합 += i;    돌아가다 합; } // 최소 홀수 완전수를 반환합니다. 인트 최소완전수(무효) {    인트 n;    위해서 (n=1; ; n+=2)       한다면 (n == 제수합(n))          돌아가다 n; }

예를 들어, 정수 1, 2, 3, …를 차례로 검색하여 홀수 완전수 등의 현상의 예를 찾을 수 있는지 확인하면 부분적으로 올바른 프로그램을 작성하는 것이 매우 쉽습니다(상자 참조).그러나 이 프로그램이 완전히 옳다고 말하는 것은 현재 숫자 이론에서 알려지지 않은 것을 주장하는 것이다.

알고리즘과 규격이 모두 공식적으로 주어진다고 가정할 때 증명은 수학적 증명이어야 합니다.특히, 이것은 주어진 기계에서 알고리즘을 구현하는 주어진 프로그램에 대한 정확성 어설션이 될 것으로 기대되지 않는다.여기에는 컴퓨터 메모리의 제한과 같은 고려사항이 포함됩니다.

증명 이론의 깊은 결과인 Curry-Howard 대응은 구성 논리에서의 기능적 정확성의 증명은 람다 미적분의 특정 프로그램에 해당한다고 말한다.이러한 방식으로 증명을 변환하는 것을 프로그램 추출이라고 합니다.

Hoare 논리는 컴퓨터 [3]프로그램의 정확성에 대해 엄격하게 추론하기 위한 특정 형식 시스템입니다.이것은 프로그래밍 언어 의미론을 정의하고 Hoare 3중으로 알려진 주장을 통해 프로그램의 정확성에 대해 논하기 위해 자명한 기술을 사용한다.

소프트웨어 테스트는 프로그램 또는 시스템의 속성 또는 기능을 평가하고 필요한 결과를 충족하는지 여부를 판단하는 것을 목적으로 하는 활동입니다.소프트웨어 품질에 중요하며 프로그래머와 테스터에 의해 널리 배포되지만 소프트웨어의 원리를 이해하는 데 한계가 있기 때문에 소프트웨어 테스트는 여전히 예술로 남아 있습니다.소프트웨어 테스트의 어려움은 소프트웨어의 복잡성에서 기인합니다.어느 정도의 복잡성으로 프로그램을 완전히 테스트할 수는 없습니다.테스트는 단순한 디버깅이 아닙니다.테스트의 목적은 품질보증, 검증 및 검증 또는 신뢰성 평가일 수 있습니다.테스트는 일반 메트릭으로도 사용할 수 있습니다.정확성 테스트와 신뢰성 테스트는 테스트의 두 가지 주요 영역입니다.소프트웨어 테스트는 예산, 시간 및 [4]품질 간의 균형입니다.

「 」를 참조해 주세요.

메모들

  1. ^ Dunlop, Douglas D.; Basili, Victor R. (June 1982). "A Comparative Analysis of Functional Correctness". Communications of the ACM. 14 (2): 229–244. doi:10.1145/356876.356881.
  2. ^ Manna, Zohar; Pnueli, Amir (September 1974). "Axiomatic approach to total correctness of programs". Acta Informatica. 3 (3): 243–263. doi:10.1007/BF00288637.
  3. ^ Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming" (PDF). Communications of the ACM. 12 (10): 576–580. CiteSeerX 10.1.1.116.2392. doi:10.1145/363235.363259. Archived from the original (PDF) on 4 March 2016.
  4. ^ Pan, Jiantao (Spring 1999). "Software Testing" (coursework). Carnegie Mellon University. Retrieved 21 November 2017.

레퍼런스