การตรวจสอบแบบคงที่แบบขยาย ( Extended static checkingหรือESC ) เป็นชื่อเรียกโดยรวมในวิทยาศาสตร์คอมพิวเตอร์สำหรับเทคนิคต่างๆ ในการตรวจสอบความถูกต้องของข้อจำกัดโปรแกรมต่างๆ แบบคงที่^{[ 1 ]} ESC สามารถคิดได้ว่าเป็นรูปแบบที่ขยายของการตรวจสอบประเภทเช่นเดียวกับการตรวจสอบประเภท ESC จะดำเนินการโดยอัตโนมัติในเวลาคอมไพล์ (กล่าวคือโดยไม่ต้องมีการแทรกแซงจากมนุษย์) ซึ่งทำให้แตกต่างจากวิธีการทั่วไปในการตรวจสอบซอฟต์แวร์อย่างเป็นทางการ ซึ่งโดยทั่วไปจะอาศัยการพิสูจน์ที่สร้างขึ้นโดยมนุษย์ ยิ่งไปกว่านั้น ESC ส่งเสริมความเหมาะสมมากกว่าความถูกต้อง โดยมีเป้าหมายเพื่อลดจำนวนผลบวกเท็จ (ข้อผิดพลาดที่ประเมินสูงเกินไปซึ่งไม่ใช่ข้อผิดพลาดจริง กล่าวคือ ESC เข้มงวดเกินไป) อย่างมาก โดยแลกกับการแนะนำ ผลลบ เท็จ บางส่วน (ข้อผิดพลาดที่ประเมินต่ำเกินไปของ ESC จริง แต่ไม่ต้องการความสนใจของโปรแกรมเมอร์ หรือไม่ได้เป็นเป้าหมายของ ESC) ^{[ 2 ] [ 3 ]} ESC สามารถระบุข้อผิดพลาดต่างๆ ที่อยู่นอกขอบเขตของตัวตรวจสอบประเภทในปัจจุบัน รวมถึงการหารด้วยศูนย์ การเข้าถึงอาร์เรย์เกินขอบเขตการล้นของจำนวนเต็มและการเข้าถึงค่าว่าง

เทคนิคที่ใช้ในการตรวจสอบแบบคงที่แบบขยายมาจากสาขาวิทยาศาสตร์คอมพิวเตอร์หลายสาขา รวมถึงการวิเคราะห์โปรแกรมแบบคงที่การจำลองเชิงสัญลักษณ์การตรวจสอบแบบจำลองการตีความแบบนามธรรมการแก้ปัญหา SATและ การ พิสูจน์ทฤษฎีบทอัตโนมัติและการตรวจสอบประเภทการตรวจสอบแบบคงที่แบบขยายโดยทั่วไปจะดำเนินการเฉพาะในระดับภายในกระบวนการ มากกว่าระดับระหว่างกระบวนการ เพื่อให้สามารถปรับขนาดไปยังโปรแกรมขนาดใหญ่ได้^{[ 2 ]} นอกจากนี้ การตรวจสอบแบบคงที่แบบขยายมีเป้าหมายเพื่อรายงานข้อผิดพลาดโดยใช้ประโยชน์จาก ข้อกำหนดที่ผู้ใช้กำหนดในรูปแบบของ เงื่อนไข ก่อนและหลัง ตัวแปรคงที่ของลูปและ ตัวแปรคง ที่ ของคลาส

โดยทั่วไปแล้ว ตัวตรวจสอบแบบสแตติกแบบขยายจะทำงานโดยการส่งต่อเงื่อนไขหลังการทำงานที่แข็งแกร่งที่สุด (หรือเงื่อนไขก่อนการทำงานที่อ่อนแอที่สุด ) ภายในกระบวนการผ่านวิธีการที่เริ่มต้นจากเงื่อนไขก่อนการทำงาน (หรือเงื่อนไขหลังการทำงาน) ในแต่ละจุดระหว่างกระบวนการนี้ จะมีการสร้างเงื่อนไขระดับกลางขึ้นมาซึ่งบันทึกสิ่งที่ทราบ ณ จุดนั้นของโปรแกรม เงื่อนไขนี้จะถูกรวมเข้ากับเงื่อนไขที่จำเป็นของคำสั่งโปรแกรม ณ จุดนั้นเพื่อสร้างเงื่อนไขการตรวจสอบตัวอย่างเช่น คำสั่งที่เกี่ยวข้องกับการหาร ซึ่งเงื่อนไขที่จำเป็นคือตัวหารต้องไม่เป็นศูนย์ เงื่อนไขการตรวจสอบที่เกิดขึ้นจากสิ่งนี้ระบุว่า: เมื่อพิจารณาจากเงื่อนไขระดับกลาง ณ จุดนี้แล้ว จะต้องสรุปได้ว่าตัวหารต้องไม่เป็นศูนย์เงื่อนไขการตรวจสอบทั้งหมดจะต้องแสดงให้เห็นว่าเป็นเท็จ (ดังนั้นจึงถูกต้องโดยวิธีการยกเว้นข้อที่สาม ) เพื่อให้วิธีการผ่านการตรวจสอบแบบสแตติกแบบขยาย (หรือ "ไม่สามารถหาข้อผิดพลาดเพิ่มเติมได้") โดยทั่วไปแล้ว จะใช้ตัวพิสูจน์ทฤษฎีบทอัตโนมัติบางรูปแบบเพื่อตรวจสอบเงื่อนไขการตรวจสอบ

การตรวจสอบแบบคงที่แบบขยายได้รับการริเริ่มใน ESC/Modula-3 ^{[ 4 ]}และต่อมาในESC/Javaรากฐานของมันมาจากเทคนิคการตรวจสอบแบบคงที่ที่เรียบง่ายกว่า เช่น การดีบักแบบคงที่^{[ 5 ]}หรือlintและFindBugsภาษาอื่นๆ อีกหลายภาษาได้นำ ESC มาใช้ รวมถึง Spec# และSPARKadaและVHDL VSPEC อย่างไรก็ตาม ปัจจุบันยังไม่มีภาษาการเขียนโปรแกรมซอฟต์แวร์ใดที่ใช้กันอย่างแพร่หลายซึ่งมีการตรวจสอบแบบคงที่แบบขยายในสภาพแวดล้อมการพัฒนาพื้นฐาน

• ภาษาสร้างแบบจำลอง Java (JML)

• Cormac Flanagan; K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata (2002). "การตรวจสอบแบบคงที่เพิ่มเติมสำหรับ Java". รายงานการประชุม ACM SIGPLAN 2002 ว่าด้วยการออกแบบและการใช้งานภาษาโปรแกรม . หน้า 234. doi : 10.1145/512529.512558 . ISBN 978-1581134636. S2CID  47141042 .{{cite book}}: CS1 maint: multiple names: authors list ( link )
• Babic, Domagoj; Hu, Alan J. (2008). "Calysto". รายงานการประชุมวิศวกรรมซอฟต์แวร์นานาชาติครั้งที่ 13 - ICSE '08หน้า 211. doi : 10.1145/1368088.1368118 . ISBN 9781605580791S2CID 62868643​ ​
• Chess, BV (2002). "การปรับปรุงความปลอดภัยของคอมพิวเตอร์โดยใช้การตรวจสอบแบบคงที่ที่ขยายเพิ่มเติม". รายงานการประชุมสัมมนา IEEE ว่าด้วยความปลอดภัยและความเป็นส่วนตัว ปี 2002หน้า  160–173 . CiteSeerX  10.1.1.15.2090 . doi : 10.1109/SECPRI.2002.1004369 . ISBN 978-0-7695-1543-4. S2CID  12067758 .
• Rioux, Frédéric; Chalin, Patrice (2006). "การปรับปรุงคุณภาพของแอปพลิเคชันองค์กรบนเว็บด้วยการตรวจสอบแบบคงที่เพิ่มเติม: กรณีศึกษา" 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). "การตรวจสอบแบบคงที่ที่ขยายได้ที่รวดเร็วและสมบูรณ์ยิ่งขึ้นสำหรับภาษาการสร้างแบบจำลอง Java" วารสาร การให้เหตุผลอัตโนมัติ44 ( 1– 2): 145– 174. CiteSeerX  10.1.1.165.7920 . doi : 10.1007/s10817-009-9134-9 . ISSN  0168-7433 . S2CID  14996225 .
• Xu, Dana N. (2006). "การตรวจสอบแบบคงที่เพิ่มเติมสำหรับ Haskell". รายงานการประชุมเชิงปฏิบัติการ ACM SIGPLAN ปี 2006 เกี่ยวกับ Haskellหน้า 48. CiteSeerX  10.1.1.377.3777 . doi : 10.1145/1159842.1159849 . ISBN 978-1595934895. S2CID  1340468 .
• Leino, K. Rustan M. (2001). "การตรวจสอบแบบคงที่ที่ขยายเพิ่มเติม: มุมมองสิบปี". สารสนเทศศาสตร์ . บันทึกการบรรยายในวิทยาการคอมพิวเตอร์. เล่มที่ 2000. หน้า  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). "การตรวจสอบแบบคงที่แบบขยาย" รายงานการวิจัย Compaq SRC (159).