Haskell 기능이 정확성 속성으로 입증 / 모델 검사 / 검증 될 수 있습니까?

Haskell 기능이 정확성 속성으로 입증 / 모델 검사 / 검증 될 수 있습니까?

---

아이디어에서 계속 : 입증 가능한 실제 언어가 있습니까?

나는 당신에 대해 모르지만 보장 할 수없는 코드를 작성하는 것에 지쳤습니다.

위의 질문을하고 경이로운 응답을받은 후 (모두 감사합니다!) 저는 Haskell 에 대한 입증 가능하고 실용적인 접근 방식을 찾기로 결정했습니다 . 실제로 유용하기 때문에 내가 하스켈을 선택 (가 많은 웹 프레임 워크 이를 위해 작성된이, 이것은 좋은 벤치 마크 것) 과 나는, 엄격한 충분하다 생각 기능적으로 그것을 증명, 또는 적어도 불변의 테스트를 허용 할 수 있음.

내가 원하는 (그리고 찾을 수 없었던)

Haskell 함수를보고 의사 코드로 작성된 추가 프레임 워크를 원합니다.

add(a, b):
    return a + b

-특정 불변성이 모든 실행 상태를 유지하는지 확인합니다. 나는 공식적인 증거를 선호하지만 모델 검사기와 같은 것에 만족할 것입니다.
이 예에서 불변성은 주어진 값 a 및 b 이고 반환 값은 항상 합계 a + b 입니다.

이것은 간단한 예이지만 이와 같은 프레임 워크가 존재하는 것은 불가능하다고 생각하지 않습니다. 확실히 테스트 할 수있는 함수의 복잡성에 대한 상한선이있을 것입니다 (함수에 대한 10 개의 문자열 입력은 확실히 오랜 시간이 걸립니다!). 이것은 함수를보다 신중하게 설계하도록 장려하고 다른 형식을 사용하는 것과 다르지 않습니다. 행동 양식. Z 또는 B를 사용한다고 상상해보십시오. 변수 / 집합을 정의 할 때 변수에 가능한 가장 작은 범위를 제공해야합니다. 당신의 INT가 100을 넘지 않을 것이라면, 그렇게 초기화해야합니다! 이와 같은 기술과 적절한 문제 분해는 Haskell과 같은 순수 기능적 언어를 만족스럽게 검사 할 수 있어야한다고 생각합니다.

나는 아직 공식적인 방법이나 Haskell에 대해 경험이 많지 않습니다. 제 아이디어가 건전한 것인지 알려주세요. 아니면 그 하스켈이 적합하지 않다고 생각 하시나요? 다른 언어를 제안하는 경우 "has-a-web-framework"테스트를 통과했는지 확인하고 원래 질문을 읽으십시오. :-)

---

글쎄, 당신이 Haskell 경로를 택하고 있기 때문에 시작해야 할 몇 가지 사항 :

• Curry-Howard 서신에 대해 잘 알고 있습니까? 이를 기반으로하는 기계 검사 증명에 사용되는 시스템은 여러면에서 매우 강력한 유형 시스템을 사용하는 단순한 기능적 프로그래밍 언어입니다.

• Haskell 코드를 분석하는 데 유용한 개념을 제공하는 추상 수학 영역에 대해 잘 알고 있습니까? 다양한 대수의 풍미와 일부 범주 이론이 많이 등장합니다.

• 모든 Turing-complete 언어와 마찬가지로 Haskell은 항상 종료되지 않을 가능성이 있습니다. 일반적으로, 무언가가 진실이거나 끝나지 않는 값에 의존 한다는 것을 증명하는 것 보다 무언가가 항상 진실 하다는 것을 증명하는 것이 훨씬 더 어렵습니다 .

단순히 테스트가 아닌 증명 을 위해 진지하게 가고 있다면 , 이것들은 명심해야 할 종류입니다. 기본 규칙은 다음과 같습니다. 잘못된 상태를 만들면 컴파일러 오류가 발생합니다. 처음부터 유효하지 않은 데이터가 인코딩되는 것을 방지 한 다음 유형 검사기가 지루한 작업을 수행하도록합니다.

더 나아가고 싶다면, 메모리가 나에게 도움이된다면 증명 보조자 인 Coq 에는 중요한 함수에 대한 임의의 속성을 증명할 수있는 "extract to Haskell"기능이 있습니다. 그러면 증명을 Haskell 코드로 바꿀 수 있습니다.

Haskell에서 직접 멋진 유형 시스템 작업을 수행하기 위해 Oleg Kiselyov는 그랜드 마스터 입니다. 그의 사이트 에서 배열 경계 검사의 정적 증명을 인코딩하는 상위 다형성 유형 과 같은 깔끔한 트릭의 예를 찾을 수 있습니다 .

더 가벼운 작업의 경우 유형 수준 인증서 를 사용하여 데이터의 정확성을 확인한 것으로 표시하는 등의 작업을 수행 할 수 있습니다 . 정확성 검사 자체는 여전히 혼자이지만 다른 코드는 적어도 일부 데이터가 실제로 검사되었음을 아는 데 의존 할 수 있습니다.

경량 검증과 멋진 유형 시스템 트릭을 구축하여 취할 수있는 또 다른 단계는 Haskell이 도메인 특정 언어 를 포함하는 호스트 언어로 잘 작동한다는 사실을 사용하는 것 입니다 . 먼저 유용한 속성을 더 쉽게 증명할 수있는 신중하게 제한된 하위 언어 (이상적으로는 Turing 완전하지 않음)를 구성한 다음 해당 DSL의 프로그램을 사용하여 전체 프로그램에서 핵심 기능의 핵심 부분을 제공합니다. 예를 들어, 해당 함수를 사용하는 항목 컬렉션의 병렬 축소를 정당화하기 위해 두 인수 함수가 연관적임을 증명할 수 있습니다 (함수 응용 프로그램의 순서는 중요하지 않으며 인수의 순서 만 중요하기 때문입니다).

---

아, 마지막으로. Haskell에 포함 된 함정을 피하는 방법에 대한 몇 가지 조언은 안전하지 않은 코드를 방해 할 수 있습니다. 여기서 맹세 한 적은 일반 재귀 , IO모나드 및 부분 함수입니다 .

• 마지막은 피하는 것이 상대적으로 쉽습니다. 작성하지 말고 사용하지 마십시오. 모든 패턴 일치 집합이 가능한 모든 경우를 처리하는지 확인하고 절대로 error또는 undefined. 유일한 까다로운 부분은 오류를 일으킬 수있는 표준 라이브러리 함수를 피하는 것입니다. 일부는 분명히 안전하지 fromJust :: Maybe a -> a않거나 head :: [a] -> a비슷하지만 다른 일부는 더 미묘 할 수 있습니다. 일부 입력 값으로 실제로는 아무것도 할 수없는 함수를 작성하는 경우 입력 유형에 의해 잘못된 상태가 인코딩되도록 허용하고이를 수정해야합니다.

• 두 번째는 IO표현식 에서 사용되는 여러 순수 함수를 통해 물건을 흩 뿌려서 피상적 인 수준에서 쉽게 피할 수 있습니다. 가능한 한 전체 프로그램을 순수한 코드로 이동하여 실제 I / O를 제외한 모든 항목과 독립적으로 평가할 수 있도록하는 것이 좋습니다. 이것은 대부분 외부 입력에 의해 구동되는 재귀가 필요할 때만 까다로워지며 최종 항목으로 이동합니다.

• 현명한 사람에게 전하는 말 : 근거가있는 재귀 와 생산적인 코어 커션. 재귀 함수가 시작점에서 알려진 기본 케이스로 이동하거나 요청시 일련의 요소를 생성하는지 항상 확인하십시오. 순수 코드에서이 작업을 수행하는 가장 쉬운 방법은 유한 데이터 구조를 재귀 적으로 축소하는 것입니다 (예 : 카운터를 최대 값까지 증가시키면서 직접 호출하는 함수 대신 카운터 값 범위를 포함하는 목록을 만들고 접는 것입니다). ) 또는 지연 데이터 구조 (예 : 어떤 값에 대한 점진적 근사치 목록)를 재귀 적으로 생성하면서 두 가지를 직접적으로 혼합하지 않습니다 (예 : "스트림에서 특정 조건을 충족하는 첫 번째 요소를 찾는 것"이 ​​아닙니다. 대신 스트림에서 최대 깊이까지 값을 가져온 다음 찾을 수없는 경우를 적절하게 처리하여 유한 목록을 검색합니다.

• 마지막 두 항목을 결합하여 IO일반적인 재귀와 함께 실제로 필요한 부분에 대해 프로그램을 증분 구성 요소로 빌드 한 다음 모든 어색한 비트를 단일 "드라이버"함수로 압축합니다. 예를 들어,와 같은 순수 함수,와 같은 mainLoop :: UIState -> Events -> UIState종료 테스트 quitMessage :: Events -> Bool, 보류중인 이벤트를 가져 오는 함수 getEvents :: IO Events및 업데이트 함수를 사용 하여 GUI 이벤트 루프를 작성한 updateUI :: UIState -> IO ()다음 실제로와 같은 일반화 된 함수로 작업을 실행할 수 runLoopIO :: (b -> a -> b) -> b -> IO a -> (b -> IO ()) -> IO ()있습니다. 이렇게하면 복잡한 부분을 진정으로 순수하게 유지하여 이벤트 스크립트로 전체 프로그램을 실행하고 결과 UI 상태를 확인할 수 있으며 어색한 재귀 I / O 부분을 이해하기 쉽고 필연적으로 정확할 수있는 단일 추상 함수로 분리 할 수 ​​있습니다. 에 의해 parametricity .

---

아마도 당신이 요구하는 것과 가장 가까운 것은 Haskabelle인데 , 이는 Haskell 파일을 Isabelle 이론으로 번역하고 그에 대한 것들을 증명할 수 있는 증명 보조 Isabelle 과 함께 제공되는 도구입니다 . 내가 이해하는 한이 도구는 HOL-ML-Haskell 프로젝트 내에서 개발되었으며 문서 페이지 에는 뒤에 숨겨진 이론에 대한 정보가 포함되어 있습니다.

저는이 프로젝트에 대해별로 익숙하지 않고 그 프로젝트로 무엇을했는지에 대해 잘 모릅니다. 하지만 저는 Brian Huffman 이 이러한 것들을 가지고 놀았다는 것을 알고 있습니다. 그의 논문과 강연을 확인하세요. 관련 내용을 포함해야합니다.

---

당신이 요청한 것이 실제로 당신을 행복하게하는 것인지는 잘 모르겠습니다. :-)

Model-checking a general purpose language is neigh impossible since models must be domain specific to be practical. Due to Gödel's Incompleteness Theorem, there simply is no method for automatically finding proofs in a sufficiently expressive logic.

This means that you have to write proofs yourself, which raises the question of whether the effort is worth the time spent. Of course, the effort creates something very valuable, namely the assurance that your program is correct. The question is not whether this is a must-have, but whether the time spent is too great a cost. The thing about proofs is that while you may have an "intuitive" understanding that your program is correct, it is often very difficult to formalize this understanding as a proof. The problem with intuitive understanding is that it's highly susceptible to accidental mistakes (typos and other stupid mistakes). This is the basic dilemma of writing correct programs.

So, research about program correctness is all about making it easier to formalize proofs and to check their correctness automatically. The programming is an integral part of the "ease of formalization"; it is very important to write programs in a style that is easy to reason about. Currently, we have the following spectrum:

• Imperative language like C, C++, Fortran, Python: Very difficult to formalize anything here. Unit tests and general reasoning are the only way to get at least some assurance. Static typing catches only trivial bugs (which much better than not catching them!).

• Purely functional languages like Haskell, ML: Expressive type system helps catch non-trivial bugs and mistakes. Proving correctness by hand is practical for snippets of up to somewhere around 200 lines, I'd say. (I did a proof for my operational package, for instance.) Quickcheck testing is a cheap substitute for formalized proofs.

• Dependently typed languages and proof assistants like Agda, Epigram, Coq: Proving whole programs correct is possible thanks to automated help with proof formalization and discovery. However, the burden is still high.

In my opinion, the current sweet spot for writing correct programs is purely functional programming. If lives depend on the correctness of your program, you better go a level higher and use a proof assistant.

---

Sounds like you want ESC/Haskell: http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm

Oh, and Agda now does have a web framework (proof of concept, at least): http://www.reddit.com/r/haskell/comments/d8dck/lemmachine_a_web_framework_in_agda/

---

Have you had a look at quickcheck? It may offer some of the things you need.

http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck

---

Your seemingly simple example, add(a,b), is actually difficult to verify - floating point, overflow, underflow, interrupts, is the compiler verified, is the hardware verified, etc.

Habit is a simplified dialect of Haskell that allows for proving program properties.

Hume is a language with 5 levels, each more limitedand therefore easier to verify:

Full Hume
  Full recursion
PR−Hume
  Primitive Recursive functions
Template−Hume
  Predefined higher−order functions
  Inductive data structures
  Inductive  Non−recursive first−order functions
FSM−Hume
  Non−recursive data structures
HW−Hume
  No functions
  Non−recursive data structures

Of course, the most popular method today for proving program properties is unit testing, which provides strong theorems, but these theorems are overly specific. "Types Considered Harmful", Pierce, slide 66

---

Have a look at Zeno. Quoting the wiki page:

Zeno is an automated proof system for Haskell program properties; developed at Imperial College London by William Sonnex, Sophia Drossopoulou and Susan Eisenbach. It aims to solve the general problem of equality between two Haskell terms, for any input value.

Many program verification tools available today are of the model checking variety; able to traverse a very large but finite search space very quickly. These are well suited to problems with a large description, but no recursive datatypes. Zeno on the other hand is designed to inductively prove properties over an infinite search space, but only those with a small and simple specification.

---

It's certainly possible to prove some properties of Haskell programs formally. I've had to do so at my FP exam: given two expressions, prove that they denote the same function. It's not possible to do this in general since Haskell is Turing-complete, so any mechanical prover would either have to be a proof assistant (semi-automatic with user guidance) or a model checker.

There have been attempts in this direction, see e.g. P-logic: property verification for Haskell programs or Proving the correctness of functional programs using Mizar. Both are academic papers describing methods more than implementations.

---

Some very recent effort by MSR Cambridge: http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf

---

The tool AProVE is (at least) able to prove termination of Haskell programs, which is part of proving correctness. More information can be found in this paper (shorter version).

Apart from that, you might be interested in Dependent Types. Here, the type system is extended and used to make wrong programs impossible.

---

You can use the tool hs-to-coq to convert Haskell mostly automatic into Coq, and then use the full power of the Coq prove assistant to verify your Haskell code. See the papers https://arxiv.org/abs/1803.06960 and https://arxiv.org/abs/1711.09286 for some more information.

참고URL : https://stackoverflow.com/questions/4077970/can-haskell-functions-be-proved-model-checked-verified-with-correctness-properti