Genişletilmiş statik kontrol - Extended static checking

Genişletilmiş statik kontrol (ESC), bilgisayar biliminde bir dizi teknik için ortak bir isimdir. statik olarak kontrol çeşitli program kısıtlamalarının doğruluğu.[1] ESC, genişletilmiş bir biçim olarak düşünülebilir. tür denetimi. Tip kontrolünde olduğu gibi, ESC otomatik olarak Derleme zamanı (yani insan müdahalesi olmadan). Bu, onu daha genel yaklaşımlardan ayırır. resmi doğrulama tipik olarak insan tarafından oluşturulan kanıtlara dayanan bir yazılım. Ayrıca, sayıyı önemli ölçüde azaltmayı amaçladığından, sağlamlığın yerine pratikliği teşvik eder. yanlış pozitifler (gerçek hata olmayan aşırı tahmin edilen hatalar, yani katılık yerine ESC) bazılarını tanıtma pahasına yanlış negatifler (gerçek ESC eksik tahmin hatası, ancak bu, programcının dikkatine ihtiyaç duymaz veya ESC tarafından hedeflenmez).[2][3] ESC, şu anda bir tür denetleyicisinin kapsamı dışında olan bir dizi hatayı belirleyebilir. sıfıra bölüm, sınırların dışında dizi, tamsayı taşması ve boş başvurular.

Genişletilmiş statik kontrolde kullanılan teknikler, çeşitli alanlardan gelir. Bilgisayar Bilimi, dahil olmak üzere statik program analizi, sembolik simülasyon, model kontrolü, soyut yorumlama, SAT çözme ve otomatik teorem kanıtlama ve tür denetimi. Genişletilmiş statik kontrol, büyük programları ölçeklendirmek için genellikle yalnızca intraprosedural seviyede (işlemler arası bir seviyede) gerçekleştirilir.[2] Ayrıca, genişletilmiş statik kontrol, kullanıcı tarafından sağlanan özellikleri kullanarak hataları şu şekilde bildirmeyi amaçlamaktadır: ön ve son koşullar, döngü değişmezleri ve sınıf değişmezleri.

Genişletilmiş statik denetleyiciler tipik olarak ilerleyerek çalışır en güçlü şartlar (resp. en zayıf ön koşullar ) ön koşuldan (ya da son koşul) başlayan bir yöntemle intraprocedural olarak. Bu işlem sırasında her noktada, o program noktasında bilinenleri yakalayan bir ara koşul oluşturulur. Bu, o noktada program bildiriminin gerekli koşullarıyla birleştirilerek bir doğrulama koşulu. Buna bir örnek, gerekli koşulu şu olan bir bölünmeyi içeren bir ifadedir: bölen sıfır olmayacak. Bundan kaynaklanan doğrulama koşulu etkili bir şekilde şunları belirtir: Bu noktada ara koşul verildiğinde, bölenin sıfır olmadığı izlenmelidir. Tüm doğrulama koşullarının yanlış olduğu gösterilmelidir (bu nedenle üçüncü hariç ) bir yöntemin genişletilmiş statik denetimi geçmesi (veya "daha fazla hata bulunamaması") için. Tipik olarak, doğrulama koşullarını boşaltmak için bir tür otomatik teorem kanıtlayıcı kullanılır.

ESC / Modula-3'te Genişletilmiş Statik Kontrol öncülüğünü yaptı[4] ve sonra, ESC / Java. Kökleri, statik hata ayıklama gibi daha basit statik kontrol tekniklerinden kaynaklanmaktadır.[5] veya Lint (yazılım) ve FindBugs. Aşağıdakiler dahil bir dizi başka dil ESC'yi benimsemiştir Teknik Özellikler # ve SPARKada ve VHDL VSPEC. Ancak, şu anda temel geliştirme ortamında genişletilmiş statik kontrol sağlayan yaygın olarak kullanılan bir yazılım programlama dili yoktur.

Ayrıca bakınız

Referanslar

  1. ^ C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe ve R. Stata. "Java için genişletilmiş statik denetim". İçinde Programlama Dili Tasarımı ve Uygulaması Konferansı Bildirileri, sayfalar 234-245, 2002. doi: http://doi.acm.org/10.1145/512529.512558
  2. ^ a b "Genişletilmiş Statik Kontrol". UWTV. Alındı 2012-02-01.[kalıcı ölü bağlantı ]
  3. ^ Calysto: Ölçeklenebilir ve Hassas Genişletilmiş Statik Kontrol, Domagoj Babic ve Alan J. Hu. Uluslararası Yazılım Mühendisliği Konferansı (ICSE) Bildirilerinde, 2008. doi:10.1145/1368088.1368118
  4. ^ Modula-3, K. Rustan M. Leino ve Greg Nelson için genişletilmiş bir Statik Denetleyici. Derleyici İnşaat Konferansı Bildirilerinde, sayfalar 302-305, 1998. doi:10.1007 / BFb0026418
  5. ^ Program değişmezlerinin ağındaki hataları yakalamak, C. Flanagan, M. Flatt, S. Krishnamurthi. S. Weirich ve M. Felleisen, sayfalar 23-32, 1996, dpi: http://doi.acm.org/10.1145/249069.231387

daha fazla okuma