디지털 논리/아키텍처 설계에 관심을 갖게 된 한 가지 사실은 자동화 된 정리 예를 들어 부동 소수점 곱셈 모듈을 검증하는 것입니다.테스트 주도 개발 대 자동 정리 입증
단위 테스트는 편리하지만 부동 소수점 모듈에 가능한 모든 입력을 테스트 (무차별 대입)하려고하면 거의 어렵지 않습니다. 대신, (1) 올바른 결과를 항상 생성한다는 증거 또는 (2) 적어도 하나의 잘못된 결과를 생성한다는 증거를 찾습니다.
저는 비슷한 논리를 제 소프트웨어에 통합하려고합니다. 테스트 주도 개발과 함께 또는 테스트 주도 개발 대신 사용할 수 있을지 궁금합니다.
'수학적으로 입증 된 소프트웨어'를 만들려고하는 것처럼 들리는데, 이는 매우 어려운 일입니다. why cant programs be proven
:
당신은 당신이 수학적 알고리즘가 정확하다는 것을 증명한다 건가요 같은 것을 할 종이를 작성하거나 코드를 작성합니까? (나는 당신이 후자를 어떻게 할 것인가에 흥미를 느끼고 있습니다 - 가능하다면 블로그 게시물이나 가능한 경우 주석에서 이것을하는 방법에 대한 설명에 링크하십시오.)
전자의 경우 테스트가 없으면 증명할 방법이 없습니다 귀하의 구현은 귀하의 의도를 반영하고 의도 한대로 작동합니다.
후자의 경우, 정리 증명 코드가 구현을 실행하지 않으면 이전 인수가 유지됩니다.
개인적으로 난 그냥 TDD를 사용하는 것 -는 나와 다른 사람 에 대한 쉽게가 아니라 필기 시험의 무리를 읽고 코드가 무엇을하는지 파악하는 원인이된다. 은 물론도 있습니다. 가능한 모든 출력을 테스트 할 필요는 없지만 대표적인 입력 집합을 식별하십시오. 각 입력은 코드를 통해 다른 결과/경로를 사용해야합니다.
하드웨어 구성 요소 (VHDL/Verilog)의 경우에도 이전에는 공식 검증에 대한 많은 경험이있었습니다. 동일한 원칙이 소프트웨어에도 적용될 수 있지만, I/O 나 이벤트가 있으면 입력 공간이 관리하기 어려워집니다. 상태 공간이 너무 커지면 커다란 "모델"에 대한 모든 종류의 성명을 증명하는 것도 비실용적입니다.
이상적으로는 "계산"기능에 대한 정리 프로 버를 사용하여 정확성을 증명할 수 있습니다. 그러나 여러 가지 이유로 테스트를 사용해야합니다.
링크를 제공해 주셔서 감사합니다! 그리고 네,이 프로젝트는 과학 계산 모델 소프트웨어입니다. – machinaut