Whiley(프로그래밍 언어)

Whiley (programming language)
와일
패러다임필수, 기능
설계자데이비드 피어스
처음 등장한2010년 6월
안정된 릴리스
0.5.0 / 2020년6월 7일, 23개월 전(2020-06-07)
타이핑 분야견고, 안전, 구조, 흐름의 영향을 받기 쉬운
면허증.BSD
웹 사이트whiley.org
영향을 받다
Java, C, Python, Rust

Whiley는 함수 패러다임과 명령 패러다임의 특징을 결합한 실험 프로그래밍 언어이며 함수 전제 조건, 사후 조건 [1]및 루프 불변량을 통해 형식 사양을 지원합니다.이 언어에서는 "플로우 타이핑"이라고도 하는 흐름에 민감한 타이핑을 사용합니다.

Whyy 프로젝트는 2003년 [2]토니 호어가 제안한 "Verifying Compiler Grand Challenge"에 따라 2009년에 시작되었습니다.Whiley의 첫 공개는 2010년 [3]6월이었다.

주로 David Pearce에 의해 개발된 Whiley는 소규모 커뮤니티에서 기여하는 오픈 소스 프로젝트입니다.이 시스템은 학생 연구 프로젝트와 학부 [4]수업에서 사용되어 왔다.그것은 2012년에서 2014년 사이에 뉴질랜드 왕립학회 Marsden [5]기금에 의해 지원되었다.

Whiley 컴파일러는 Java 가상 머신의 코드를 생성하여 Java 및 기타 JVM 기반 언어와 상호 운용할 수 있습니다.

개요

Whiley의 목표는 검증이 일상적이고 아무 생각 없이 사용되는 현실적인 프로그래밍 언어를 제공하는 것입니다.이러한 툴의 아이디어는 오랜 역사를 가지고 있지만 2000년대 초에 Hoare의 Verifying Compiler Grand Challenge를 통해 강력하게 홍보되었습니다.이 과제의 목적은 검증 컴파일러 개발에 박차를 가하는 것입니다.[6]개략적으로 설명하면 다음과 같습니다.

검증 컴파일러는 수학적 논리적 추론을 사용하여 컴파일하는 프로그램의 정확성을 확인합니다.

--

이러한 툴의 주된 목적은 프로그램이 정식 사양을 충족하도록 함으로써 소프트웨어의 품질을 향상시키는 것입니다.Whiley는 SPARK/Ada, ESC/Java, Spec#, Dafny, Why3,[7] Frama-C와 같은 중요한 노력을 포함하여 이러한 툴을 개발하기 위한 많은 시도를 수행하고 있습니다.

대부분의 이전 시도를 프로토 완성 차 컴파일러를 개발하기 위해 구문과 규격을 쓰기 위해 기존 프로그래밍 언어를 확장시키는데 초점을 맞추다.예를 들어, ESC/Java과 자바 모델링 언어 자바에 전제 조건과 postconditions을 지정하기 위한 주석 기관.마찬가지로, Spec#및 Frama-C은 C#및 C프로그래밍 언어와 비슷한 구문을 추가한다.하지만, 이 언어들은 확인을 위해 또는 극복할 수 없는 어려운 문제를 수많은 기능을 포함한다고 알려져 있다.[8]이와는 대조적으로, Whiley 언어 처음부터 노력 및 검증 더 다루기 쉽게 일반적인 문제들을 피할 수 있도록 설계되었다.[9]

특징들

Whiley의 구문 또는 객체 지향 명령형 언어의 일반적인 모양을 따른다.Indentation 구문 교정을 묘사하다. 성명 블록을 사용, 파이선을 방불케에 대해 선택된다.로 언어와 순수한 기능적이다 하지만, Whiley의 명령 룩 다소 오해의 소지가 있습니다.

Whiley 구별functiona로부터(이는 순수한는)method(는 부작용이 있을 것).로 기능 규격에서 사용될 수 있도록 이 차이는 필요하다.기본 데이터 형식에 가까운 집합이 있는.bool,int, 배열(예를 들어int[])과 기록(예를 들어{int x, int y}대부분의 프로그래밍 언어와는 달리). 그러나 정수 데이터 type,.int는 무제한이며 32비트2의 보완과 같은 고정폭 표현에 대응하지 않습니다.따라서 Whiley의 제약 없는 정수는 호스트 환경의 메모리 제약 조건에 따라 가능한 모든 정수 값을 취할 수 있습니다.이 선택은 모듈로 산술에 대한 추론이 알려진 어려운 문제이기 때문에 검증을 단순화합니다.복합 객체(예: 배열 또는 레코드)는 Java 또는 C# 등의 언어로 되어 있기 때문에 힙 상의 값에 대한 참조가 아니라 불변의 값입니다.

Whiley는 "플로우 타이핑"이라고 불리는 유형 검사에 대해 특이한 접근 방식을 취합니다.변수는 함수 또는 메서드의 서로 다른 지점에서 서로 다른 정적 유형을 가질 수 있습니다.플로우 타입은 [10]Racket에서 볼 수 있는 오카렌스 타입과 비슷합니다.흐름 입력을 지원하기 위해 Whiley는 결합,[11] 교차 및 부정 유형을 지원합니다.결합 유형은 Haskell과 같은 함수 언어에서 볼 수 있는 총합 유형과 비슷하지만 Whiley에서는 분리되지 않습니다.교차 및 부정 유형은 흐름 유형의 컨텍스트에서 런타임 유형 테스트의 참 및 거짓 분기 변수 유형을 결정하기 위해 사용됩니다.예를 들어, 변수가x타입의T및 런타임 유형 테스트x is S. 진정한 브랜치에서는,x된다T & S반면, 잘못된 가지에서는T & !S.

Whiley는 공칭이 아닌 구조형 시스템을 사용합니다.Modula-3, Go 및 Ceylon은 어떤 형태로든 구조 타자를 지원하는 다른 언어의 예입니다.

반면, Rust에서 볼 수 있는 것과 유사한 기준 수명을 지원합니다.새 개체를 할당할 때 안전하게 할당 해제될 수 있는 시기를 나타내는 수명을 지정할 수 있습니다.그런 다음 이러한 오브젝트에 대한 참조에는 참조가 행잉되지 않도록 라이프타임 식별자가 포함되어야 합니다.모든 메서드에는 에 의해 참조되는 암묵적인 라이프타임이 있습니다.this. 유형 변수&this:T유형 객체에 대한 참조를 나타냅니다.T에워싸는 메서드로 할당 해제됩니다.수명 간의 서브타이핑은 수명 관계에 따라 결정됩니다.따라서,&l1:T의 서브타입입니다.&l2:T만약 평생 동안l1정적으로 수명을 연장하다l2그 범위가 다른 범위를 감싸는 일생은 그 범위보다 오래 산다고 한다.Whiley의 수명은 현재 소유권 개념이 없다는 점에서 Rust와 다릅니다.

Whiley는 동시성을 지원하지 않으며 공유 가변 상태에 대한 읽기/쓰기를 어떻게 해석해야 하는지를 결정하는 공식 메모리 모델도 없습니다.

예

다음 예시는 Whiley의 많은 흥미로운 기능을 보여줍니다.여기에는 사후 조건, 루프 불변량, 유형 불변량, 결합 유형 및 흐름 유형이 포함됩니다.이 함수는 정수의 첫 번째 인덱스를 반환하기 위한 것입니다.item정수 배열로items. 그러한 인덱스가 존재하지 않는 경우null이 반환됩니다. 

// 자연수의 종류를 정의합니다. 유형 내트 이 (인트 x) 어디에 x >= 0  일반의 기능. 색인(인트[] 항목들, 인트 아이템) -> (인트 무효 색인) // int가 반환된 경우 이 위치의 요소는 항목과 일치합니다. 보증하다 색인 이 인트 ==> 항목들[색인] == 아이템 // int가 반환된 경우 이 위치의 요소가 처음 일치합니다. 보증하다 색인 이 인트 ==> 아니요. { i 에 0 .. 색인   항목들[i] == 아이템 } // null이 반환된 경우 항목에 일치하는 요소가 없습니다. 보증하다 색인 이 무효 ==> 아니요. { i 에 0 ..  항목들    항목들[i] == 아이템 }:     //     내트 i = 0     //     하는 동안에 i < >  항목들      // 항목과 일치하는 요소가 없습니다.     어디에 아니요. { j 에 0 .. i   항목들[j] == 아이템 }:         //         한다면 항목들[i] == 아이템:             돌아가다 i         i = i + 1     //     돌아가다 무효

위에서 함수의 선언된 반환 유형에는 유니언 유형이 지정됩니다.int null그 말은, 어느쪽이든int값이 반환되거나null이 반환됩니다.함수의 사후 조건은 3가지로 구성됩니다.ensures각 절은 반환된 각 절을 보유해야 하는 서로 다른 속성을 기술합니다.index흐름 타입은 런타임타입의 test 연산자를 통해 이들 절에서 사용됩니다.is예를 들어, 처음에ensures절, 변수index에서 재입력되었습니다.int null딱 맞게int암시 연산자의 오른쪽에 있습니다(예:==>).

위의 예에서는 유도 루프 불변량의 사용도 나타내고 있습니다.루프 불변수는 루프의 임의의 반복 및 루프가 종료될 때 루프의 엔트리를 보류하도록 표시해야 합니다.이 경우, 루프 불변성은 다음과 같은 요소에 대해 알려진 것을 나타냅니다.items지금까지의 조사에서는, 즉, 어느 것도 소정의 것과 일치하지 않습니다.item루프 불변성은 프로그램의 의미에 영향을 주지 않으며, 어떤 의미에서는 불필요한 것으로 간주될 수 있습니다.단, 루프 불변수는 Whiley 컴파일러에서 이 함수가 사양을 충족함을 증명하기 위해 사용하는 자동 검증기를 지원하기 위해 필요합니다.

위의 예에서는 타입도 정의하고 있습니다.nat적절한 유형 불변성을 갖는 것.이 유형은 변수를 선언하는 데 사용됩니다.i절대 음의 값을 유지할 수 없음을 나타냅니다.이 경우 선언은 형식의 불변 루프 추가의 필요성을 방지합니다.where i >= 0그렇지 않았다면 필요했을 겁니다

역사

2009년에 첫 공개를 시작으로v0.2.272010년 6월에 이어v0.3.0그 해 9월에.그 언어는 오늘날까지 수많은 구문적 변화가 이루어지면서 서서히 발전해 왔다.이전 버전v0.3.33서포트되고 있는 퍼스트 클래스string그리고.char데이터 타입은 삭제되었지만 스트링을 제약으로 표현하기 위해 삭제되었습니다.int[]어레이.마찬가지로 이전 버전도v0.3.35지원되는 퍼스트 클래스 세트(예:{int}사전(예:{int=>bool}) 및 크기 조정 가능한 목록[int]단, 단순 어레이를 위해 폐기되었습니다(예:int[]아마도 가장 논란이 많았던 것은 의 제거였을 것이다.real버전의 데이터 유형v0.3.38이러한 변경의 대부분은 언어를 단순화하고 컴파일러 개발을 보다 관리하기 쉽게 만들고자 하는 바람에서 비롯되었습니다.

Whiley의 진화에 있어 또 하나의 중요한 이정표는 버전입니다.v0.3.40세바스찬 슈와이저가 카이저슬라우테른 대학의 석사 논문의 일부로 개발한 참조 수명을 포함시켰다.

레퍼런스

  1. ^ "Whiley Homepage".
  2. ^ Hoare, Tony (2003). "The Verifying Compiler: A Grand Challenge for Computing Research". Journal of the ACM. 50: 63–69. doi:10.1145/602382.602403. S2CID 441648.
  3. ^ "Whiley v0.2.27 Released!".
  4. ^ "whiley.org/people".
  5. ^ "Marsden Fund".
  6. ^ Hoare, Tony (2003). "The Verifying Compiler: A Grand Challenge for Computing Research". Journal of the ACM. 50: 63–69. doi:10.1145/602382.602403. S2CID 441648.
  7. ^ "Why3 --- Where Programs Meet Provers".
  8. ^ Barnett, Mike; Fähndrich, Manuel; Leino, K. Rustan M.; Müller, Peter; Schulte, Wolfram; Venter, Herman (2011). "Specification and verification: the Spec# experience". Communications of the ACM. 54 (6): 81. doi:10.1145/1953122.1953145. S2CID 29809.
  9. ^ Pearce, David J.; Groves, Lindsay (2015). "Designing a Verifying Compiler: Lessons Learned from Developing Whiley". Science of Computer Programming. 113: 191–220. doi:10.1016/j.scico.2015.09.006.
  10. ^ "Occurrence Typing".
  11. ^ Pearce, David (2013). "Sound and Complete Flow Typing with Unions, Intersections and Negations" (PDF).