ATS(프로그래밍 언어)

ATS (programming language)
ATS
The ATS Logo.svg
패러다임멀티탭: 기능, 필수
설계자보스턴 대학교 홍웨이자이 교수
안정된 릴리스
ATS2-0.4.2[1] / 2020년 11월 14일, 20개월 전(2020-11-14)
타이핑 분야정적인
면허증.GPLv3
파일 이름 확장자.sats, .dats, .dats
웹 사이트http://www.ats-lang.org/
영향을 받다
종속 ML, ML, OCaml, C++

ATS(Applied Type System)는 프로그래밍을 정식 사양과 통합하도록 설계된 프로그래밍 언어입니다.ATS는 고급형 [2]시스템을 사용하여 정리 증명과 실제 프로그래밍을 결합하는 것을 지원합니다.The Computer Language Benchmarks Game의 과거 버전은 ATS의 성능이 C [3]및 C++ 프로그래밍 언어의 성능과 동등하다는 것을 증명했습니다.정리 증명과 엄격한 타입 체크를 사용함으로써 컴파일러는 프로그램 컴파일 전에 포인터 산술과 참조 카운트를 검증함으로써 구현된 함수가 제로 나눗셈, 메모리 리크, 버퍼 오버플로 및 기타 형태의 메모리 파손 등의 버그에 취약하지 않음을 검출하고 증명할 수 있다.또한 프로그래머는 ATS(ATS/LF)의 통합정리프로비저닝시스템을 사용함으로써 함수가 사양에 도달했음을 증명하기 위해 연산코드에 얽힌 정적구조를 사용할 수 있다.

역사

ATS는 대부분 ML 및 OCaml 프로그래밍 언어에서 파생됩니다.이전 언어인 Dependent ML은 동일한 저자의 언어로 통합되었습니다.

ATS1(Anairiats)의 최신 버전은 2015년 1월 [4]20일에 v0.2.12로 출시되었습니다.ATS2(Postiats)의 첫 [5]버전은 2013년 9월에 출시되었습니다.

정리 증명

ATS의 주요 초점은 실용적인 [2]프로그래밍과 조합하여 정리 증명을 지원하는 것입니다.정리를 증명하면 예를 들어 구현된 함수가 메모리 누수를 발생시키지 않는다는 것을 증명할 수 있습니다.또한 테스트 중에만 발견될 수 있는 다른 버그를 방지합니다.일반적으로 수학적 증명만을 목적으로 하는 증명 보조자의 시스템과 유사한 시스템을 포함하고 있다. 단, ATS는 이 기능을 사용하여 기능의 구현이 올바르게 동작하고 예상 결과를 산출한다.

간단한 예로서 나눗셈을 사용하는 함수에서 프로그래머는 제수가 결코 0이 되지 않는다는 것을 증명할 수 있으며, 0에 의한 나눗셈을 방지할 수 있다.예를 들어, 제수 'X'가 목록 'A'의 5배 길이로 계산되었다고 합시다.리스트가 비어 있지 않은 경우, X는 0이 아닌 두 숫자(5와 A의 길이)의 곱이기 때문에 X가 0이 아니라는 것을 증명할 수 있다.보다 실용적인 예는 할당된 메모리 블록의 유지 카운트가 각 포인터에 대해 올바르게 카운트되고 있음을 참조 카운트를 통해 증명하는 것입니다.그러면 오브젝트가 너무 빨리 할당 해제되지 않고 메모리 누수가 발생하지 않음을 문자 그대로 알 수 있습니다.

ATS 시스템의 장점은 모든 정리 증명은 컴파일러 내에서 엄격하게 이루어지기 때문에 실행 가능한 프로그램의 속도에 영향을 미치지 않는다는 것입니다.ATS 코드는 표준 C 코드보다 컴파일이 어려운 경우가 많지만 컴파일러와 런타임 시스템이 올바르다고 가정하고 컴파일을 하면 프로그래머는 증명서에 의해 지정된 범위까지 올바르게 실행되고 있는지 확인할 수 있습니다.

ATS에서 증명은 구현과 별개이므로 프로그래머가 원한다면 증명하지 않고 함수를 구현할 수 있다.

data 표현

저자(Hongwei Xi)에 따르면 ATS의 효율성은[6] 주로 언어와 테일콜 최적화(일반적으로 기능 프로그래밍 언어의 효율성에 중요)로 데이터를 표현하는 방식에 기인합니다.데이터는 박스형 표현이 아닌 플랫형 또는 언박스형 표현으로 저장할 수 있습니다.

정리 증명:도입 사례

명제

dataprop는 술어를 대수형으로 나타냅니다.

ATS 소스와 다소 유사한 의사 코드로 술어(유효한 ATS 소스에 대해서는 아래 참조): 

FACT(n, r) ifff fact(n) = r MUL(n, m, prod) ifff n * m = prod FACT(n, r) = FACT(0, 1) if f FACT(n-1, r1) 및 MUL(n, r1, r) if fact(n, r) = rf fact(nf fact(nf = rf = rf)

ATS 코드:

 데이터 처리 사실 (인트, 인트) =      팩트베이스 (0, 1)             // 기본의 사례.: 사실(0, 1)      {n:인트   n > 0} {r,r1:인트} // 귀납적 사례.      팩트인드 (n, r) 의 (사실 (n-1, r1), 멀티 (n, r1, r))

여기서 FACT(int, int)는 증명 유형입니다.

예

제안 또는 "Theorem"이 시공 데이터프로프를 통해 증명되는 비꼬리 반복 요인.

의 평가fact1(n-1)쌍을 반환하다(proof_n_minus_1 result_of_n_minus_1)계산에서 사용된다.fact1(n)증명은 명제의 술어를 표현한다.

파트 1 (알고리즘과 명제)

[FACT (n, r)]는 [fact (n) = r][MUL (n, m, prod)]는 [n * m = prod]를 의미한다.
FACT(0, 1) FACT(n, r) ifff FACT(n-1, r1) 및 MUL(n, r1, r) (모든 n > 0)

주의사항:

{...} 범용 수량화 [...] 실존 수량화(...) (증거값) @(...) 플랫 태플 또는 가변 함수 매개 변수 태플 .<...> 종료[7] 메트릭
#포함하다 "share/atspre_staload.disples"  데이터 처리 사실 (인트, 인트) =     팩트베이스 (0, 1) 의 () // 기본의 사례.     {n:내트}{r:인트}       // 귀납적 사례.     팩트인드 (n+1, (n+1)*r) 의 (사실 (n, r))  (*) int(x)는 int x 값의 모노값 타입입니다.  다음 함수 시그니처는 다음과 같습니다. all n:nat, exists r:int. 여기서 fact(num:int(n)는 (FACT(n, r)int(r)*)를 반환합니다.  재밌어요 사실{n:내트} .<n> 。 (n: 인트 (n)) : [r:인트] (사실 (n, r)   인트(r)) = (   케이스     n > 0 => ((팩트인드(pf1)   n * r1)) 어디에    {      값 (pf1   r1) = 사실 (n-1)   }     _(*syslog*) => (팩트베이스()   1) )

파트 2(루틴 및 테스트)

시행하다 메인 0 (argc, argv) = {   값 () = 한다면 (argc != 2) 그리고나서 프리! ("사용방법: ", argv[0], "<filename>")    값 () = 주장하다 (argc >= 2)   값 n0 = g0string2int (argv[1])   값 n0 = g1ofg0 (n0)   값 () = 주장하다 (n0 >= 0)   값 (_(*pf*)   인식하다) = 사실 (n0)    값 ((*syslog*)) = 인쇄! ("사실상, n0, ") = ", 인식하다) }

이 모든 것을 하나의 파일에 추가하고 다음과 같이 컴파일할 수 있습니다.컴파일은 다양한 백엔드 C 컴파일러(gcc 등)와 연동해야 합니다.가비지 컬렉션은 다음과 같이 명시적으로 명시되지 않는 한 사용되지 않습니다.-D_ATS_GCATS） [8]。 

$ patscc fact1 . dats -o fact1 $ / fact1 4

컴파일하여 기대한 결과를 제공하다

특징들

기본형

  • bool(참, 거짓)
  • int(리터럴: 255, 0377, 0xFF), ~(ML에서와 같이)의 단수 마이너스
  • 이중으로 하다
  • 문자 'a
  • 스트링 "timeout"

튜플 및 레코드

prefix @ 또는 none은 직접, 플랫 또는 박스가 없는 할당을 의미합니다.
  값 x : @(인트, 차) = @(15, 'c')  // x.0 = 15 ; x.1 = 'c'   값 @(a, b) = x                    // 양식 매칭 바인딩, a= 15, b='c'   값 x = @{첫번째=15, 둘째='c'}    // x.첫번째 = 15   값 @{첫번째=a, 둘째=b} = x       // a= 15, b='c'   값 @{둘째=b, ...} = x           // 와 함께 누락, b='c'
prefix '는 간접 또는 박스형 할당을 의미합니다.
  값 x : '(인트, 차) = '(15, 'c')  // x.0 = 15 ; x.1 = 'c'   값 '(a, b) = x                    // a= 15, b='c'   값 x = '{첫번째=15, 둘째='c'}    // x.첫번째 = 15   값 '{첫번째=a, 둘째=b} = x       // a= 15, b='c'   값 '{둘째=b, ...} = x           // b='c'
스페셜

'를 구분자로 지정하면 일부 함수는 결과 값을 술어 평가로 래핑합니다.

val ( fredicate _ fredicate values )= myfacted params

흔한

{...} 범용 수량화 [...] 존재 수량화 (...) 상위 표현식 또는 태플 (...) (표준값)
.<...>종단 메트릭 @(...) 플랫태플 또는 바리안트 함수 파라미터 태플(예시의 printf) 참조 @[ byte ][BUFLEN]타입[9] 바이트의 BUFLEN 값 배열 @[ byte ][BUFLEN]() 어레이 인스턴스 @[ byte ][BUFLEN](0) 어레이가 0으로 초기화됨

사전

sort:domain
sortdef nat = {a: int a > = 0 } // 전주곡부터: int a int... 
typedef String = [ a : nat ]스트링(a) // [..] : " nat ..."
type (as sort)
매개 변수화된 다형 함수에 사용되는 포인터 단어의 길이를 가진 요소의 일반 정렬.또, 「상자 [10]타입」도 있습니다. 
// {..}: "a,b" 유형...fun {a,b:type} swap_type_type(xy: @(a, b): @(b, a) =(xy.1, xy.0)
t@ype
길이가 추상화된 이전 유형의 선형 버전입니다.또한 개봉된 [10]유형입니다.
viewtype
뷰가 있는 도메인 클래스 타입(메모리 어소시에이션)
viewt@ype
길이가 추상화된 뷰타입의 선형 버전.뷰 타입을 슈퍼셋합니다.
view
타입과 메모리 위치의 관계.인픽스@는 가장 일반적인 컨스트럭터입니다.
T @ L로케이션 L에 타입 T의 뷰가 있다고 단언합니다.
 재밌어요 {a:t@이페} ptr_get0 {l:주소} (pf: a @ l   p: ptr l): @(a @ l   a)    재밌어요 {a:t@이페} ptr_set0 {l:주소} (pf: a? @ l   p: ptr l, x: a): @(a @ l   무효)
의 종류ptr_get0 (T)이∀ l : addr . ( T @ l ptr( l ) ) -> ( T @ l T) // see manual, section 7.1. Safe Memory Access through Pointers[11]
viewdef array_v (a:viewt@ype, n:int, l:addr) = @[a][n] @ l
T?
초기화되지 않은 유형일 수 있음

패턴 매칭 완전성

예를 들어 case+, val+, type+, viewtype+, ...

  • 서픽스 '+'를 붙이면 컴파일러는 완전하지 않은 대체의 경우 오류를 발생시킵니다.
  • 서픽스를 붙이지 않으면 컴파일러가 경고를 발행합니다.
  • 접미사로 '-'를 사용하면 소모량 조절을 피할 수 있습니다.

모듈

staload "foo.sats" // foo.sats가 로드된 후 현재 네임스페이스 staload F = "foo.sats" //에 열려 $F.bar dynload "foo.dats" // 런타임에 동적으로 로드된 식별자를 사용합니다.

데이터 표시

데이터뷰는 종종 선형 [12]리소스에서 재귀적으로 정의된 관계를 인코딩하도록 선언됩니다.

dataview array_v (a: viewt@ype+, int, addr) = {l: addr} array_v_none (a, 0, l) {n: addr} array_v_some (a, n+1, l) / (a @ l, array_v (a, n+size of a))

데이터형/데이터뷰형

데이터형[13]

datatype workday = 월화수금

리스트

datatype list0 (a:t@ype) = (a, list0 a) list0_cons (a)

데이터 뷰 타입

데이터 보기 유형은 데이터 유형과 비슷하지만 선형입니다.dataviewtype을 사용하면 프로그래머는 dataviewtype과 [14]관련된 컨스트럭터를 저장하기 위해 사용되는 메모리를 안전한 방법으로 명시적으로 해방(또는 할당 해제)할 수 있다.

변수

지역 변수

var res: int with pf_res = 1 // 뷰의 에일리어스로 pf_res가 도입되었습니다.@ ( res )

스택 어레이 할당 시:

#pf_buf = @[ byte ]의 BUFLEN 10 var !p_buf [BUFLEN](0) // pf_buf = @[ byte ][부플렌](0) @ p_buf[15]

val 및 var[16] 선언 참조

레퍼런스

  1. ^ Hongwei Xi (14 Nov 2020). "[ats-lang-users] ATS2-0.4.2 released". ats-lang-users. Retrieved 17 Nov 2020.
  2. ^ a b 프로그래밍과 정리 증명 결합
  3. ^ ATS 벤치마크 컴퓨터 언어 벤치마크 게임(Web 아카이브)
  4. ^ "The ATS PL System - Browse /Ats-lang at SourceForge.net".
  5. ^ "Updating: Adding a release file. · githwxi/ATS-Postiats@30fd556". GitHub.
  6. ^ 언어의 효율성에 대한 토론(Language Shoothing: ATS는 새로운 최고의 총잡이입니다.C++를 능가합니다).
  7. ^ 종료 메트릭
  8. ^ 컴파일 - 가비지 컬렉션 2009년8월 4일 Wayback Machine에서 아카이브 완료
  9. ^ 2011년 9월 4일 아카이브된 어레이 타입, 예를 들어 @[T][ Wayback Machine ][나]
  10. ^ a b "Introduction to Dependent types". Archived from the original on 2016-03-12. Retrieved 2016-02-13.
  11. ^ 매뉴얼, 섹션 7.1 포인터를 통한[permanent dead link] 안전한 메모리 액세스(구식)
  12. ^ Dataview 구축 2010년 4월 13일 Wayback Machine에서 아카이브 완료
  13. ^ 데이터형 컨스트럭트 2010년 4월 14일 웨이백 머신에서 아카이브 완료
  14. ^ Dataviewtype 구성
  15. ^ 수동 - 7.3 스택 메모리 할당 2014년 8월 9일 Wayback Machine에서 보관(구식)
  16. ^ 2014년 8월 9일 Wayback Machine에 보관된 Val 및 Var 선언(구식)

외부 링크

Wikibooks는 다음과 같은 주제에 관한 책을 가지고 있습니다: ATS: Programming with Orginary-Proving