확장 스태틱 체크
Extended static checking확장 정적 검사(ESC)는 컴퓨터 과학에서 다양한 프로그램 제약 [1]조건의 정확성을 정적으로 검사하는 일련의 기술을 총칭하는 것입니다.ESC는 유형 확인의 확장된 형태라고 생각할 수 있습니다.유형 확인과 마찬가지로 ESC는 컴파일 시(즉, 사람의 개입 없이) 자동으로 수행됩니다.이는 일반적으로 인간이 생성한 증거에 의존하는 소프트웨어의 공식적인 검증에 대한 보다 일반적인 접근법과는 구별된다.또, 일부의 부정(실제 ESC 과소 평가 에러)을 도입해, 프로그래머의 주의를 필요로 하지 않거나, ESC의 대상이 되지 않는 부정(실제 에러가 아닌 추정 에러)의 수를 큰폭으로 삭감하는 것을 목적으로 하는 건전성보다 실용성을 촉진한다.) ESC는 0으로 나눗셈, 배열 범위 외, 정수 오버플로, 늘 참조 등 현재 유형 체커의 범위를 벗어난 일련의 오류를 식별할 수 있습니다.[2][3]
확장 정적 검사에 사용되는 기술은 정적 프로그램 분석, 기호 시뮬레이션, 모델 검사, 추상 해석, SAT 해결 및 자동 정리 증명 및 유형 검사를 포함한 컴퓨터 과학의 다양한 분야에서 유래합니다.확장 정적 검사는 일반적으로 대규모 프로그램으로 [2]확장하기 위해 절차 간 수준이 아닌 절차 간 수준에서만 수행됩니다.또한 확장 정적 체크는 사전 및 사후 조건, 루프 불변성 및 클래스 불변성의 형태로 사용자가 제공한 규격을 이용하여 오류를 보고하는 것을 목적으로 합니다.
확장 정적 체커는 일반적으로 전제 조건(응답 후 조건)에서 시작하는 방법을 통해 절차적으로 가장 강력한 사후 조건(응답 후 조건)을 전파함으로써 작동한다.이 프로세스 중에 각 시점에서 해당 프로그램 포인트에서 알려진 내용을 캡처하는 중간 조건이 생성됩니다.이를 프로그램 스테이트먼트의 필요조건과 조합하여 검증조건을 형성합니다.예를 들어 나눗셈을 포함하는 문장이며, 나눗셈의 필요조건은 제수가 0이 아니라는 것입니다.여기서 발생하는 검증 조건은 실질적으로 명시되어 있습니다.이 시점에서 중간 조건이 주어지면 제수가 0이 아님을 따라야 합니다.메서드가 확장 정적 검사를 통과하려면(또는 "더 이상의 오류를 찾을 수 없음") 모든 검증 조건이 거짓임을 보여야 합니다(따라서 제외된 세 번째 방법으로 수정).전형적으로 검증 조건을 해제하기 위해 어떤 형태의 자동 정리 프로버가 사용됩니다.
확장 스태틱 체크는 ESC/Modula-3[4], 그 후 ESC/Java에서 개척되었습니다.그 뿌리는 정적[5] 디버깅이나 린트(소프트웨어) 및 FindBugs와 같은 보다 단순한 정적 체크 기술에서 비롯되었습니다.Spec#, SPARKada, VHDL VSPEC 등 많은 언어가 ESC를 채택하고 있습니다.그러나 현재 기본 개발 환경에서 확장된 정적 체크를 제공하는 널리 사용되는 소프트웨어 프로그래밍 언어는 없습니다.
「 」를 참조해 주세요.
- Java 모델링 언어(JML)
레퍼런스
- ^ C. Flanagan, K.R.M. Leino, M. Lilibridge, G. Nelson, J. B. Saxe 및 R.Stata. "Java에 대한 확장된 정적 검사"프로그래밍 언어 설계 및 구현에 관한 회의의 의사록, 234-245, 2002.doi: http://doi.acm.org/10.1145/512529.512558
- ^ a b "Extended Static Checking". UWTV. Retrieved 2012-02-01.[영구 데드링크]
- ^ Babic, Domagoj; Hu, Alan J. (2008). Calysto: Scalable and Precise Extended Static Checking. Proceedings of the International Conference on Software Engineering (ICSE). ACM Press. doi:10.1145/1368088.1368118.
- ^ Rustan, K.; Leino, M.; Nelson, Greg (1998). "An extended static checker for modula-3". Lecture Notes in Computer Science - International Conference on Compiler Construction. Springer. pp. 302–305. doi:10.1007/bfb0026441. ISBN 978-3-540-64304-3. ISSN 0302-9743.
- ^ Flanagan, Cormac; Flatt, Matthew; Krishnamurthi, Shriram; Weirich, Stephanie; Felleisen, Matthias (1996). "Catching bugs in the web of program invariants" (PDF). ACM SIGPLAN Notices. Association for Computing Machinery (ACM). 31 (5): 23–32. doi:10.1145/249069.231387. ISSN 0362-1340.
추가 정보
- Cormac Flanagan; K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata (2002). Extended static checking for Java. Proceedings of the Conference on Programming Language Design and Implementation (PLDI). p. 234. doi:10.1145/512529.512558. ISBN 978-1581134636.
{{cite book}}: CS1 maint: 여러 이름: 작성자 목록(링크) - Babic, Domagoj; Hu, Alan J. (2008). Calysto: Scalable and Precise Extended Static Checking. Proceedings of the International Conference on Software Engineering (ICSE). p. 211. doi:10.1145/1368088.1368118. ISBN 9781605580791.
- Chess, B.V. (2002). Improving computer security using extended static checking. Proceedings of IEEE Symposium on Security and Privacy. pp. 160–173. CiteSeerX 10.1.1.15.2090. doi:10.1109/SECPRI.2002.1004369. ISBN 978-0-7695-1543-4.
- Rioux, Frédéric; Chalin, Patrice (2006). "Improving the Quality of Web-based Enterprise Applications with Extended Static Checking: A Case Study". Electronic Notes in Theoretical Computer Science. 157 (2): 119–132. doi:10.1016/j.entcs.2005.12.050. ISSN 1571-0661.
- James, Perry R.; Chalin, Patrice (2009). "Faster and More Complete Extended Static Checking for the Java Modeling Language". Journal of Automated Reasoning. 44 (1–2): 145–174. CiteSeerX 10.1.1.165.7920. doi:10.1007/s10817-009-9134-9. ISSN 0168-7433.
- Xu, Dana N. (2006). Extended static checking for haskell. Proceedings of the ACM Workshop on Haskell. p. 48. CiteSeerX 10.1.1.377.3777. doi:10.1145/1159842.1159849. ISBN 978-1595934895.
- Leino, K. Rustan M. (2001). Extended Static Checking: A Ten-Year Perspective. Informatics. Lecture Notes in Computer Science. Vol. 2000. pp. 157–175. doi:10.1007/3-540-44577-3_11. ISBN 978-3-540-41635-7.
- Detlefs, David L.; Leino, K. Rustan M.; Nelson, Greg; Saxe, James B. (1998). "Extended Static Checking". Compaq SRC Research Report (159).
