많은 언어 (아마도 모든 언어)는 프로그램 작성을 쉽게하기 위해 고안되었습니다. 그들 모두는 다른 영역을 가지고 있으며, 이러한 영역에서 프로그램 개발을 단순화하고자합니다. C는 저수준 프로그램을 쉽게 개발하고 Java는 복잡한 비즈니스 논리를 쉽게 개발할 수 있도록합니다. 아마도 더 쉽고 자연스럽고 오류가 발생하기 쉬운 방식으로 프로그램을 작성하고 유지하기 위해 다른 목적이 희생되었을 것입니다.정적으로 쉽게 확인하도록 설계된 언어
소스 코드를 확인하기 위해 특별히 설계된 언어가 있습니까? 정적 분석 - 쉽게? 물론 최신 기계에 대한 공통 프로그램을 작성하는 기능도 지속되어야합니다.
가, 내가 나 자신을 사용하지 않은 정적 분석 중간 언어 또는 Flexibo
" Inermediate languages "는 일반적으로 서로 다른"프로덕션 언어 "와 검증 도구를 중재하는 것입니다. 원래 프로그램을 어떤 식 으로든 제한하지 않으므로 검증이 더 좋지 않습니다. –
SAIL, 그래서 나는 어떤 권위를 가지고 말할 수 없다,하지만 난 에펠 프로그래밍 언어 코드를 사용하도록 설계되었습니다 이해 계약에 의해 정적 분석을 훨씬 쉽게 할 수 있습니다. 그게 중요하지 않은지 나는 모른다.
계약서를 지정하는 것은 관련이 있고 (아마도, 필요할 수도 있지만), 내가 물어 보는 언어에는 충분하지 않습니다. –
특히 소스 코드를 쉽게 확인하도록 설계된 언어가 있습니까?
이것은 CLU와 ML 언어 모두 막연한 목표 였지만, 정적 검증을 정말 진지하게 생각한 유일한 언어 디자인은 Spark Ada입니다.
Dijkstra의 언어 보호 명령 (프로그래밍 분야에 설명되어 있음)은 정적 검증을 지원하도록 설계되었지만 명시 적으로 구현되지 않아야합니다.
Gerard Holzmann의 Promela 언어도 모델 검사기 SPIN에서 정적 분석을 위해 설계되었지만 실행이 불가능합니다.
"소스 코드를 쉽게 검증"하는 데는 두 가지 문제점이 있습니다. 하나는 임의의 경우 (예 : C)와 같은 사소한 일을하지 않는 언어입니다. 또 다른 하나는 이며 확인하려는 내용은입니다. 좋은 어설 션 언어가 필요하기 때문입니다.
많은 언어가 그러한 어설 션 언어를 제안했지만, EDA 커뮤니티는 시간적 사양으로 가장 효과적으로 봉투를 밀고 있다고 생각합니다. "특성 명세 언어"는 표준입니다. P1850 Standard for PSL: Property Specification Language (IEEE-1850)에서 자세히 알아볼 수 있습니다. PSL의 한 가지 아이디어는 기존 EDA 언어에 추가 할 수 있다는 것입니다. 시간이 지남에 따라 EDA 공동체가 EDA langauges에 통합되었다고 생각합니다.
저는 종종 PSL과 같은 것이 일반적인 컴퓨터 소프트웨어에 포함되기를 바랬습니다.
Auditors (E 언어)은 언어 자체에 코드 분석을 작성하고 일부 코드 섹션이 일부 정적 검사를 통과해야한다는 기본 제공 수단을 제공합니다.또한이 논문의 관련 업무에 관심이있을 수 있습니다.
정적 인증은이 작업의 시작점이 아닙니다. 이는 프로그램의 정확성을 자동으로 검증 할 수 있다는 전제에 기반합니다. 현실 세계에서는 실현 가능하지 않으며, 프로그램이 어떤 힌트없이 임의로 복잡한 코드를 검사 할 것으로 기대하는 것은 단순한 바보입니다. 일반적으로 정적 검증을위한 소프트웨어는 결국 소스 코드 전체에 힌트를 필요로하며 결국에는 오 탐지 (false positive) 및 위음성 (false negative)을 많이 생성합니다. 그것은 틈새 시장을 가지고 있지만 그게 전부입니다. (Pierce의 "Types and programming languages"에 대한 소개 참조)
이러한 종류의 도구는 엔지니어가 단순한 목적으로 개발 한 것이지만 실제 솔루션은 아카데미에서 베이킹되었습니다. 정적으로 타입이 지정된 프로그래밍 언어의 유형은 모든 것이 원활하게 진행되고 언어에 어떤 종류의 나쁜 동작이없는 것으로 가정하면 논리 문장과 동일하다는 것을 알 수 있습니다. 이것을 "Curry-Howard correspondence"이라고 부르며 유형에 논리를 삽입하는 것은 "Brouwer-Heyting-Kolmogorov logic"입니다. 가장 강력한 증명은 강력한 유형의 언어 인 dependent types에서만 가능합니다. 이 용어를 모두 잊어 버리면, programs that carry proofs의 정확성을 기록 할 수 있으며, 프로그램이 컴파일되는 동안 이러한 증명이 검사되며, 실패한 경우 실행 파일이 제공되지 않습니다.
이 접근 방식의 긍정적 인 측면은 사용자가 절대로 false negatives을 얻지 못한다는 것입니다. 즉, 컴파일 된 프로그램은 사양에 따라 올바르게 작동한다는 보장이 있습니다. 명세에 대한 추가적인 증거가 없다하더라도, 의존형 언어로 된 프로그램은 오류가 발생하기 쉽지 않습니다. 왜냐하면 실행 가능 프로그램에서 처리되지 않는 예외, 처리되지 않은 예외 및 오버 플로우가 절대로 발생하지 않기 때문입니다.
항상 손으로 그러한 교정본을 작성하는 것은 지루합니다. 이를 위해 "tactics"즉 정확성의 교정본을 생성하는 프로그램이 있습니다. 이것들은 정적 검증을위한 프로그램과 거의 동일하지만, 그것들과 달리 공식적인 증명을 생성해야합니다. Coq, Agda, Idris, Epigram, Cayenne 등
전술이 COQ에서 구현 아마도 몇 가지 더 많은 언어됩니다
는 서로 다른 목적을 위해 의존적-으로 입력 된 언어의 범위가있다. 또한 Coq는 가장 성숙했으며, Bedrock과 같은 라이브러리를 포함한 인프라가 있습니다. COQ의 경우 C 코드를 추출에서
는 C.
Haskell의 성능에 파에 ATS를 사용할 수 있습니다, 귀하의 요구 사항에 충분하지 않다 카레 - 하워드 대응의 약한 양식을 사용 : 잘 작동, 실패하거나 영원히 루핑하는 프로그램을 작성하지 않는 한. 요구 사항이 공식 증명을 작성하는 것이 어렵지 않은 경우 Haskell 사용을 고려하십시오.
정적 분석을하거나 도구를 통해 더 쉽게 분석 할 수 있도록 고안된 언어를 의미합니까? 내 대답은 다른 사람들이 의미하는 것과는 다른 것처럼 보입니다. 아마도 나는 틀 렸습니다. 그러나 질문을 다시 읽음으로써이 모호성의 여지가 있습니다. – jdehaan
@jdehaan을 사용하면 도구를 쉽게 사용할 수 있습니다. 즉, 해당 언어로 구현 된보다 쉬운 분석 프로그램 *을 만들 수 있습니다. "정적 검증 도구를 구현하는 언어"가 아닙니다. –
고마워요, 그럼 내 대답을 무시해 주셔서 감사합니다, 당신을 위해 유용하지 않으며, 또한 내가 인용 언어는 매우 실험적이며 이론적 인 작업 이외의 것들에 유용하지 않습니다. 나는 누군가가 그것을 흥미로워 할지도 모른다 :-) – jdehaan