유형분석

Typestate analysis

프로토콜 분석이라고도 불리는 유형 분석은 프로그래밍 언어에 사용되는 프로그램 분석의 한 형태다.그것은 객체 지향 언어에 가장 일반적으로 적용된다.타이페스트는 주어진 유형의 인스턴스에 대해 수행할 수 있는 유효한 작업 순서를 정의한다.타이페스트는 이름에서 알 수 있듯이 상태 정보를 해당 유형의 변수와 연관시킨다.이 상태 정보는 형식의 인스턴스에 대해 호출할 수 있는 유효한 작업을 컴파일할 때 결정하는 데 사용된다.일반적으로 런타임에만 실행될 수 있는 객체에 대해 수행되는 연산은 객체의 새로운 상태와 호환되도록 수정된 형식 상태 정보에 따라 수행된다.

타이페스트는 "방법 B가 호출되기 전에 방법 A가 호출되어야 하며, 방법 C는 그 사이에 호출되지 않을 수 있다"와 같은 행동 유형 개선을 나타낼 수 있다.타이페스트는 파일을 열린 상태로 두는 것과 같은 유효하지 않은 시퀀스와 반대로 "열린 후 닫기"와 같은 의미론적으로 유효한 시퀀스를 시행함으로써 열린/닫기 의미론을 사용하는 리소스를 나타내는 데 적합하다.그러한 자원은 파일 시스템 요소, 트랜잭션, 연결 및 프로토콜을 포함한다.예를 들어, 개발자들은 파일이나 소켓을 읽거나 쓰기 전에 반드시 열어야 하며, 파일이나 소켓을 닫은 경우에는 더 이상 읽거나 쓸 수 없도록 지정하기를 원할 수 있다."일반 부동산"이라는 명칭은 이러한 종류의 분석이 종종 유한 상태 기계로서 각 유형의 물체를 모델링한다는 사실에서 유래한다.이 상태 기계에서 각 상태는 잘 정의된 허용 방법/메시지 집합을 가지며, 메서드 호출이 상태 전환을 일으킬 수 있다.페트리 그물 또한 정교화 유형과 함께 사용할 수 있는 가능한 행동 모델로 제안되었다.[1]

타이프로스테이트 분석은 롭 스트롬이 1983년[2] IBM 왓슨랩에서 개발한 네트워크 구현 언어(NIL)에서 도입했다.그것은 1986년[3] 기사에서 스트롬과 예미니가 타이프로스테이트를 사용하여 변수의 초기화 정도를 추적하고, 부적절하게 초기화된 데이터에 연산이 적용되지 않도록 보장하며, 헤르메스 프로그래밍 언어로 더욱 일반화되었다.

최근 몇 년 동안, 다양한 연구들이 객체 지향 언어에 오타이트 개념을 적용하는 방법을 개발했다.[4][5]

접근하다

유형의 변수를 초기화할 때 발생하는 비선형 오타이트 격자.
최소 요소 ⊥은 초기화된 구조 구성요소가 없는 상태 ∅과 일치한다.

스트롬과 예미니(1986)는 특정 유형의 타이피스트 세트를 일부 정보를 삭제하여 상위 유형에서 더 낮은 오타를 얻을 수 있도록 부분적으로 주문할 것을 요구했다.예를 들어,intC의 변수에는 일반적으로 "비초기화" < "초기화"가 있고FILE*포인터에는 "할당되지 않음" < "할당되지 않음, 그러나 초기화되지 않음" < "할당되지 않음, 그러나 파일이 열리지 않음" < 파일이 열림"이라는 오타가 있을 수 있다.더욱이 스트롬과 예미니는 각 두 타이피스트의 하한선이 가장 크도록 요구한다. 즉, 부분 순서는 심지어 만남-세밀라티시(meet-semilatice)일 뿐이며, 각 오더는 항상 "상호"라고 불리는 최소 요소를 가져야 한다.

이들의 분석은 각 변수 v에 프로그램 텍스트의 각 포인트에 대해 하나의 오타입체만 할당된다는 단순화에 근거한다. p 포인트는 서로 다른 두 개의 실행 경로로 도달하고 v가 각 경로를 통해 서로 다른 오타를 상속받는 경우 p에서 v의 오타입체는 상속된 오타입체 중 가장 낮은 하한값으로 간주된다.예를 들어, 다음 C 조각에서 변수는n으로부터 「initialized」와「uninit」의 오타를 상속받다.then그리고 (기호)else부분, 따라서 전체 조건문 뒤에 각각 "입체화"가 있다. 

인트로 n;                // 여기서 n은 "입체화됨"을 가지고 있다. 만일 (...) {     n = 5;            // 여기, n은 오타스테이트 "substitution"이 있다. } 다른 {     /*아무것도 하지마*/    // 여기서 n은 "입체화됨"을 가지고 있다. }                     // 여기서 n은 유형자산 "입체화" = greatest_lower_boundbound","initialized")를 가지고 있다.

모든 기본 운용에는[note 1] 유형자산 전환(즉, 각 매개변수에 대해 각각 운용 전/후에 요구되는 유형자산과 보장된 유형자산)이 장착되어야 한다.예를 들어, 수술fwrite(...,fd)필요로 하다fd"파일 열기"를 위해 오타스테이트를 가지고 있다.더 정확히 말하면, 수술은 몇 가지 결과를 가질 수 있으며, 각각의 결과는 자체적인 오타지 전환이 필요하다.예를 들어, C 코드는FILE *fd=fopen("foo","r")놓다fd의 "파일 열기" 및 "할당되지 않음" 유형(개방 성공 및 실패 시)

각각의1 두 오타2 t에 대해, 오타 t의2 대상에 적용할 때, 일부 자원을 방출함으로써 오타를 t로1 줄이는 독특한 오타 강요 수술이 제공되어야 한다.예를 들어,fclose(fd)강요하다fd의 "파일 열기"에서 "파일 열기"에서 "열리지 않음"으로 오타이트.

프로그램 실행은 다음과 같은 경우 typeesty-correct라고 불린다.

  • 각 기본 운영 전에, 모든 매개변수는 운영의 유형자산 전환에 필요한 유형자산을 정확히 가지고 있다.
  • 프로그램 종료 시, 모든 변수는 유형자산 ⊥[note 2]에 있다.property)에 있다.

프로그램 텍스트는 조정기 흐름에 의해 허용된 경로가 오타-정확한 것으로 오타가 정적으로 표시될 수 있는 프로그램에 적절한 오타 강제성을 추가하여 변환될 수 있는 경우 오타-정합성이라고 불린다.스트롬과 예미니는 주어진 프로그램 텍스트의 오타를 확인하는 선형 시간 알고리즘을 부여하고, 만약 있다면 어떤 강제 연산을 삽입해야 하는지를 계산한다.

과제들

정확하고 효과적인 오용 분석을 달성하기 위해서는 앨리어싱 문제를 해결할 필요가 있다.앨리어싱은 객체가 객체를 가리키는 기준 또는 포인터를 두 개 이상 가지고 있을 때 발생한다.분석이 정확하려면, 주어진 객체에 대한 상태 변화를 해당 객체를 가리키는 모든 참조에 반영해야 하지만, 일반적으로 그러한 모든 참조를 추적하는 것은 어려운 문제다.이것은 특히, 분석이 나머지 프로그램을 고려하지 않고 큰 프로그램의 각 부분에 개별적으로 적용 가능해야 하는 모듈화가 필요한 경우에 더욱 어려워진다.

또 다른 문제로서, 일부 프로그램의 경우, 실행 경로 수렴 시 최대 하한을 취하고 그에 상응하는 다운-코션 연산을 추가하는 방법이 불충분해 보인다.예를 들어, 이전에return 1다음 프로그램에서 [note 3]모든 구성 요소x,y그리고z의coord초기화가 되었지만, 루프 본체에 있는 구조 구성요소의 각 초기화는 첫 번째 루프 엔트리의 유형인 viz를 만족시키기 위해 루프 재진입 시 다운코싱되어야 하기 때문에, 스트롬과 예미니의 접근방식은 이것을 인식하지 못한다.⊥. 관련 문제는 이 예제가 예를 들어, 유형전환의 과부하를 필요로 한다는 것이다.parse_int_attr("x",&coord->x)"초기화되지 않은 구성 요소"를 "x 구성 요소 초기화"로 변경하고 "y 구성 요소 초기화"를 "x 및 y 구성 요소 초기화"로 변경한다. 

인트로 parse_joord(구조상의{인트로 x;인트로 y;인트로 z;} *좌표) {     인트로 보이는 = 0;     /* 어떤 속성을 파싱했는지 기억 */     하는 동안에 (1)         만일      (parse_int_attr("x",&좌표->x)) 보이는 = 1;         다른 만일 (parse_int_attr("Y",&좌표->y)) 보이는 = 2;         다른 만일 (parse_int_attr("z",&좌표->z)) 보이는 = 4;         다른 부숴뜨리다;     만일 (보이는 != 7)    /* 일부 특성 누락, 실패 */         돌아오다 0;     ...               /* 모든 속성이 존재하며, 일부 계산을 수행하고 성공 */     돌아오다 1; }

오용 추론

프로그램(또는 계약과 같은 다른 유물)에서 오타를 추론하려는 몇 가지 접근법이 있다.그들 중 다수는 컴파일 시간에 오타를 추론할 수 있고 다른 이들은 모델을 동적으로 채굴할 수 있다.[10][11][12][13][14][15]

오타를 지원하는 언어

타이프로스테이트는 아직 주류 프로그래밍 언어로 넘어가지 않은 실험적인 개념이다.그러나, 많은 학술 프로젝트들은 어떻게 하면 그것을 일상적인 프로그래밍 기법으로 더 유용하게 만들 수 있을 것인가에 대해 적극적으로 조사한다.두 가지 예로 카네기멜론 대학의 조나단 알드리히 그룹에 의해 개발되고 있는 플라이드와 오브시디안 언어가 있다.[16][17]다른 예로는 클라라어[18] 연구 프레임워크, 이전 버전의 러스트어, 그리고 더 많은 언어들이 있다.>>ATS의 키워드.[19]

참고 항목

메모들

  1. ^ 이것들은 언어구성을 포함한다. 예를 들어)이 포함된다.+=C 및 표준 라이브러리 루틴(예:fopen()
  2. ^ 이는 예를 들어 모든 파일이 닫히고 모든 파일이 닫혔는지 확인하는 것을 목적으로 한다.malloc기억력이 아주 좋아졌다.freed. 대부분의 프로그래밍 언어에서 변수의 수명은 프로그램 종료 전에 끝날 수 있다. 오타입체-정확성의 개념은 그에 따라 날카로워져야 한다.
  3. ^ 라고 가정하여int parse_int_attr(const char *name,int *val)초기화하다*val성공할 때마다

참조

  1. ^ Jorge Luis Guevara D´ıaz (2010). "Typestate oriented design - A coloured petri net approach" (PDF).
  2. ^ Strom, Robert E. (1983). "Mechanisms for compile-time enforcement of security". Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '83. pp. 276–284. doi:10.1145/567067.567093. ISBN 0897910907.
  3. ^ Strom, Robert E.; Yemini, Shaula (1986). "Typestate: A programming language concept for enhancing software reliability" (PDF). IEEE Transactions on Software Engineering. IEEE. 12: 157–171. doi:10.1109/tse.1986.6312929.
  4. ^ DeLine, Robert; Fähndrich, Manuel (2004). "Typestates for Objects". ECOOP 2004: Proceedings of the 18th European Conference on Object-Oriented Programming. Lecture Notes in Computer Science. Springer. 3086: 465–490. doi:10.1007/978-3-540-24851-4_21. ISBN 978-3-540-22159-3.
  5. ^ Bierhoff, Kevin; Aldrich, Jonathan (2007). "Modular Typestate Checking of Aliased Objects". OOPSLA '07: Proceedings of the 22nd ACM SIGPLAN Conference on Object-Oriented Programming: Systems, Languages and Applications. 42 (10): 301–320. doi:10.1145/1297027.1297050. ISBN 9781595937865.
  6. ^ Guido de Caso, Victor Braberman, Diego Garbervetsky, Sebastian Uchitel. 2013.동작 유효성 검사를 위한 활성화 기반 프로그램 추상화.ACM Trans.소프트웨. 엥.방법론. 22조, 3조, 25조 (2013년 7월), 46쪽.
  7. ^ R. 알루르, P. 세니, P. 마드후수단, W. 남.자바 클래스의 인터페이스 사양 종합, 제32회 프로그래밍 언어 원리 심포지엄, 2005
  8. ^ Giannakopoulou, D, C.S. Pasaranu, "JavaPathfinder에서의 인터페이스 생성 및 구성 검증", FASE 2009.
  9. ^ 토마스 A.헨징어, 란지트 얄라, 루팍 마금다르.허용 인터페이스.제13회 연례 소프트웨어 엔지니어링 재단 심포지엄(FSE), ACM Press, 2005, 페이지 31-40의 진행.
  10. ^ 발렌틴 달마이어, 크리스티안 린디그, 안드르제즈 와실코스키, 안드레아스 젤러.ADABU를 사용한 마이닝 객체 동작.Dynamic Systems 분석에 관한 2006년 국제 워크숍의 진행 (WODA '06).ACM, 뉴욕, 뉴욕, 미국, 17-24
  11. ^ 카를로 게찌, 안드레아 모찌, 마티아 몽가.2009. 그래프 변환에 의한 강도 높은 행동 모델 합성.제31회 소프트웨어 엔지니어링 국제 회의(ICSE '09)의 진행 중.IEEE 컴퓨터 협회, 워싱턴 DC, 미국, 430-440
  12. ^ 마크 가벨과 전동 수 2008.시간적 사양의 상징적 채굴.소프트웨어 엔지니어링에 관한 제30차 국제 회의의 절차서 (ICSE '08)에서.ACM, 뉴욕, 뉴욕, 미국, 51-60
  13. ^ 다비드 로렌졸리, 레오나르도 마리안리, 마우로 페제 2008.소프트웨어 행동 모델의 자동 생성.소프트웨어 엔지니어링에 관한 제30차 국제 회의의 절차서 (ICSE '08)에서.ACM, 뉴욕, 미국, 501-510
  14. ^ 이반 베샤스트니크, 유리 브런, 시구르드 슈나이더, 마이클 슬론, 마이클 D.2011년 에른스트기존 계측기를 활용하여 불변 제약 모델을 자동으로 추론.제19회 ACM SIGSoft 심포지엄 및 제13회 유럽 소프트웨어 엔지니어링 재단 회의(ESEC/FSE '11)에서.ACM, 뉴욕, 뉴욕, 미국, 267-277
  15. ^ Pradel, M.; Gross, T.R., "대형 방법 추적으로부터 객체 사용 명세 자동 생성," Automated Software Engineering, 2009.ASE '09. 24차 IEEE/ACM 국제회의 , vol, no. 페이지 371,382, 2009년 11월 20일
  16. ^ Aldrich, Jonathan. "The Plaid Programming Language". Retrieved 22 July 2012.
  17. ^ Coblenz, Michael. "The Obsidian Programming Language". Retrieved 16 February 2018.
  18. ^ Bodden, Eric. "Clara". Retrieved 23 July 2012.
  19. ^ Xi, Hongwei. "Introduction to Programming in ATS". Retrieved 20 April 2018.