6
A
답변
7
COQ은 올바른 ocaml 출력을 생성하는 증명 보조자입니다. 그래도 꽤 복잡합니다. 나는 주변을 둘러 보지 못했지만 동료는 2 달 후 사용을 시작했다가 사용을 중단했습니다. 대부분 일을 더 빨리 끝내기를 원했기 때문에 가능했지만 알고리즘을 검증해야 할 필요가 있다면 좋은 생각 일 수 있습니다.
Here is a course은 COQ를 사용하고 알고리즘 증명에 대해 이야기합니다.
및 here is a tutorial은 COQ에서 학술 논문 작성에 관한 것입니다.
+0
여기, http://www.lix.polytechnique.fr/coq/getting-started – nlucaroni
2
일반적으로 정확성 증명은 현재 사용중인 알고리즘에 따라 다릅니다.
그러나 사용 된 후 재사용되는 몇 가지 잘 알려진 트릭이 있습니다. 예를 들어 재귀 알고리즘의 경우 loop invariants을 사용할 수 있습니다.
또 다른 일반적인 트릭은 원래의 문제를 알고리즘의 정확성 증명이 더 쉽게 표시 할 수있는 문제로 줄인 다음 더 쉬운 문제를 일반화하거나 더 쉬운 문제를 원래의 문제에 대한 솔루션으로 변환 할 수 있음을 보여줍니다. Here은 설명입니다.
특정 알고리즘을 염두에 둔다면 일반적인 대답이 아닌 해당 알고리즘의 증명을 구성하는 방법을 묻는 것이 좋습니다.
+0
알고리즘 감소 (특히 링크에서 설명한대로))는 문제가 적어도 다른 문제만큼 어렵다는 것을 입증하는 이론적 도구입니다. Turing machine 계산 모델에서 종종 수행되는 이러한 증명은 손으로 물결 치는 업무이며 형식적 (machine-checkable) 증명과는 아무런 관련이 없습니다. 실제로 문제를 해결하기 위해 실제로 문제를 해결하기 위해 수행됩니다 (링크의 예는 Halting 문제에 대한 것으로, 알려진 NP-hard 문제를 줄임으로써 NP-hard 문제가 있음을 보여줍니다). 간추려서, 나는 문제의 축소가 공식적인 정확성과 관련이 있다는 것을 확신하지 못한다. –
+0
어쩌면 축소가 내가 여기서 사용해야하는 정확한 용어가 아닐 수도 있습니다. 내가 감축을 말할 때 나는 다음의 예를 따라 뭔가를 의미했습니다. 당신이 알고있는 N 개의 직사각형의 교차를 계산하는 알고리즘을 가지고 있다고 가정 해보십시오. N 개의 직사각형의 교차점을 계산하는 문제에 대해이 문제의 간단한 해석이 존재하는 또 다른 문제가 있다고 가정 해보십시오. 그런 다음 첫 번째 알고리즘을 사용하여 후자의 문제에 대한 솔루션을 계산합니다.남아있는 것은 모두 번역이 정확한지 보여줍니다. – ldog
+0
하지만 이것이 혼란 스럽다는 것을 알 수 있습니다.이 알고리즘은 올바른 것으로 알려진 알고리즘 (이 경우 N 개의 사각형을 계산하는 알고리즘)을 사용한다는 사실에 의존합니다. 이것이 올바른 알고리즘을 증명하거나 제공하는 방법인지 여부에 관해 혼란이 어디에서 발생하는지 확인하십시오. – ldog
2
알고리즘의 정확성을 검증하는 것이 사양에 대한 적합성을 확인하는 것이라고 생각합니다. 이론적 컴퓨터 과학 분야의 한 곳인 Formal Methods이 있습니다. 가능한 한 증명에 가까워 져야하는 경우 찾고있는 것이 될 수 있습니다. 위키 피 디아에서
정형 기법은 특정 종류의 사양, 개발을위한 수학적 기반 기술의 및 소프트웨어와 하드웨어의 검증 시스템
있습니다
당신은 많은 학습을 찾을 수있을 것입니다 링크 된 위키 피 디아 페이지와 Formal Methods wiki에있는 수많은 링크의 리소스와 도구를 사용하십시오.
2
는이 책을 구매 : http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800
Gries 책, 과학 프로그램이 좋은 물건입니다. 환자는 철저하고 완전합니다.
4
- 그것은 일반적으로 쉽게는 부작용이 관련되지 않은 경우 정확성을 증명/확인하는 많은,하지만 그것은 절대적인 요건이 아니다.
- Z과 같은 공식적인 사양 언어에 대해서는 설명서를 참조 할 수 있습니다. 공식 표준은 증명 그 자체가 아니지만, 종종 하나의 표준이됩니다.
+0
그리고 Z가 마음에 든다면 정식으로 올바른 알고리즘을 작성하는 과정에서이를 통합 할 수있는 도구를 찾을 수 있다고 확신하십시오. http : //www.bmethod.com/php/methode-b-en.php –
1
Huth와 Ryan의 컴퓨터 과학 논리는 시스템을 검증하기위한 최신 시스템에 대한 합리적인 가독성 개요를 제공합니다.옛날 옛적에 사람들은 부작용이있을 수도 있고 없을 수도있는 프로그래밍 언어로 올바른 프로그램 증명에 관해 이야기했습니다. 이 책과 다른 곳에서 얻은 인상은 실제 응용 프로그램이 다르다는 것입니다. 예를 들어 프로토콜이 맞는지 또는 칩의 부동 소수점 단위가 올바르게 나눌 수 있는지 또는 연결된 목록을 조작하기위한 잠금없는 루틴이 올바른지 등입니다.
ACM Computing Surveys Vol41 Issue 4 (2009 년 10 월)는 소프트웨어 검증에 관한 특별 쟁점입니다. "공식 방법 : 실습 및 경험"을 검색하여 ACM 계정없이 적어도 하나의 논문에 갈 수있는 것 같습니다.
+0
"공식 방법"은 귀하가 언급 한 모든 목표를 포함합니다. 저는 "올바른 프로그램을 증명하는"하위 분야에 있습니다. 그리고 지금까지 큰 산업의 성공은 다른 하위 분야에서 왔습니다 (내년까지 기다려주십시오!). FMWEEK와 같은 회의는 이러한 다양한 접근 방식과 목표를 가진 사람들을 모으기 때문에 다소 수수께끼 같지만 우리는 공통점이 많고 많은 것을 교환해야합니다. –
1
Elazar가 주석에서 데모 비디오를 제안하는 도구 ACSL은 함수 계약 작성을위한 사양 언어와 C 함수가 부재와 같은 계약 및 안전 속성을 충족하는지 확인하기위한 다양한 분석기를 제공합니다 런타임 오류가 발생했습니다.
확장 된 자습서 ACSL by example은 실제 C 알고리즘의 지정 및 검증 예제를 보여 주며 부작용이없는 함수를 효과가있는 함수와 분리합니다. 부작용이없는 함수는 더 쉽게 간주되며 지도 시간). 이 문서는 또한 설명하는 도구의 디자이너가 작성하지 않았기 때문에 흥미 롭습니다. 따라서이 기술을 더 신선하고 교훈적으로 볼 수 있습니다. 프로그래밍의 http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html
1
당신은 확실히 ACL2을 확인해야합니다. 간단한 작업은 Wirth의 체계적 프로그래밍으로, 간단한 사용 방법으로 시작됩니다. Wirth는 언어에 대해 사전 ISO Pascal을 사용합니다. Dijkstra는 Guarded (GCL)라고하는 Algol-68과 같은 형식을 사용합니다. 공식 검증은 Dijkstra와 Hoare 이후 성숙되었지만,이 오래된 텍스트는 여전히 좋은 출발점이 될 수 있습니다.
1
다 익스트라의 징계를 그의 EWDS 프로그래밍의 과학 공식적인 검증을위한 기반을 마련 : 당신은 LISP에 익숙하다면
0
스탠포드 친구들이 개발 한 PVS 도구는 사양 및 검증 시스템입니다. 나는 그것을 연구하고 Theoram Proving에 매우 유용하다는 것을 알았습니다.
0
WRT (1)와 같이 상태 기반 부작용을 모델로하는 프로그램 변수에서 알고리즘의 부작용을 "포착"하는 방식으로 알고리즘 모델을 작성해야합니다.
부작용에 대해 무슨 뜻인지 모르겠습니다. – ldog
참조 : http://en.wikipedia.org/wiki/Side_effect_%28computer_science%29 – joemoe
좋은 답변이있는 http://stackoverflow.com/questions/476959/why-cant-programs-be-proven을 참조하십시오. –