Rozszerzone sprawdzanie statyczne

Rozszerzone sprawdzanie statyczne ( ESC ) to zbiorcza nazwa w informatyce dla szeregu technik statycznego sprawdzania poprawności różnych ograniczeń programu. ESC można traktować jako rozszerzoną formę sprawdzania typu . Podobnie jak w przypadku sprawdzania typu, ESC jest wykonywane automatycznie w czasie kompilacji (tj. bez interwencji człowieka). To odróżnia ją od bardziej ogólnych podejść do formalnej weryfikacji oprogramowania, które zazwyczaj opierają się na dowodach generowanych przez ludzi. Ponadto przedkłada praktyczność nad solidność, ponieważ ma na celu radykalne zmniejszenie liczby fałszywych trafień (przeszacowanych błędów, które nie są prawdziwymi błędami, to znaczy nadmiernej ścisłości ESC) kosztem wprowadzenia niektórych fałszywych negatywów (rzeczywisty błąd niedoszacowania ESC, ale które nie wymagają uwagi programisty lub nie są celem ESC). ESC może zidentyfikować zakres błędów, które są obecnie poza zakresem sprawdzania typu, w tym dzielenie przez zero , tablica poza granicami , przepełnienie liczb całkowitych i dereferencje zerowe .

Techniki stosowane w rozszerzonym sprawdzaniu statycznym pochodzą z różnych dziedzin informatyki, w tym statycznej analizy programów , symulacji symbolicznych , sprawdzania modeli , interpretacji abstrakcyjnej , rozwiązywania testów SAT oraz automatycznego dowodzenia twierdzeń i sprawdzania typów . Rozszerzone sprawdzanie statyczne jest generalnie wykonywane tylko na poziomie wewnątrz procedury, a nie między procedurami, w celu skalowania do dużych programów. Ponadto rozszerzone sprawdzanie statyczne ma na celu zgłaszanie błędów poprzez wykorzystanie specyfikacji dostarczonych przez użytkownika w postaci wstępnych i końcowych , niezmienników pętli i niezmienników klas .

Rozszerzone sprawdzanie statyczne zazwyczaj działa poprzez propagowanie najsilniejszych warunków końcowych (odpowiednio najsłabszych warunków wstępnych ) wewnątrz procedury za pomocą metody rozpoczynającej się od warunku wstępnego (odpowiednio warunku końcowego). W każdym punkcie tego procesu generowany jest warunek pośredni, który obejmuje to, co jest znane w tym punkcie programu. Jest to połączone z niezbędnymi warunkami instrukcji programu w tym punkcie, aby utworzyć warunek weryfikacyjny . Przykładem tego jest stwierdzenie obejmujące dzielenie, którego warunkiem koniecznym jest, aby dzielnik był różny od zera. Warunek weryfikacji wynikający z tego skutecznie stwierdza: biorąc pod uwagę warunek pośredni w tym momencie, musi z tego wynikać, że dzielnik jest niezerowy . Aby metoda przeszła rozszerzone sprawdzanie statyczne (lub „nie można znaleźć więcej błędów”), wszystkie warunki weryfikacji muszą być fałszywe (a więc poprawne za pomocą wykluczonej trzeciej ). Zazwyczaj do spełnienia warunków weryfikacji używana jest jakaś forma automatycznego dowodzenia twierdzeń.

Rozszerzone sprawdzanie statyczne było pionierem w ESC/Modula-3, a później w ESC/Java . Jego korzenie wywodzą się z prostszych technik sprawdzania statycznego, takich jak debugowanie statyczne lub Lint (oprogramowanie) i FindBugs . Wiele innych języków przyjęło ESC, w tym Spec# i SPARKada oraz VHDL VSPEC. Jednak obecnie nie ma powszechnie używanego języka programowania oprogramowania, który zapewnia rozszerzone sprawdzanie statyczne w podstawowym środowisku programistycznym.

Zobacz też

• Język modelowania Java (JML)

Dalsza lektura

•    Cormaca Flanagana; K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata (2002). Rozszerzone sprawdzanie statyczne dla języka Java . Materiały z konferencji na temat projektowania i wdrażania języka programowania (PLDI) . P. 234. doi : 10.1145/512529.512558 . ISBN 978-1581134636 . S2CID 47141042 . {{ cite book }} : CS1 maint: wiele nazwisk: lista autorów ( link )
•    Babić, Domagoj; Hu, Alan J. (2008). Calysto: skalowalne i precyzyjne rozszerzone sprawdzanie statyczne . Materiały z Międzynarodowej Konferencji Inżynierii Oprogramowania (ICSE) . P. 211. doi : 10.1145/1368088.1368118 . ISBN 9781605580791 . S2CID 62868643 .
•     Szachy, BV (2002). „Poprawa bezpieczeństwa komputera za pomocą rozszerzonego sprawdzania statycznego”. Proceedings 2002 Sympozjum IEEE na temat bezpieczeństwa i prywatności . Obrady Sympozjum IEEE na temat bezpieczeństwa i prywatności . s. 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). „Poprawa jakości internetowych aplikacji korporacyjnych dzięki rozszerzonemu sprawdzaniu statycznemu: studium przypadku” . Notatki elektroniczne w informatyce teoretycznej . 157 (2): 119–132. doi : 10.1016/j.entcs.2005.12.050 . ISSN 1571-0661 .
•     James, Perry R.; Chalin, Patrice (2009). „Szybsze i pełniejsze rozszerzone sprawdzanie statyczne języka modelowania Java” . Dziennik automatycznego rozumowania . 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). „Rozszerzone sprawdzanie statyczne dla haskell” . Materiały z warsztatów ACM SIGPLAN 2006 na Haskell - Haskell '06 . Materiały z warsztatów ACM na temat Haskella . P. 48. CiteSeerX 10.1.1.377.3777 . doi : 10.1145/1159842.1159849 . ISBN 978-1595934895 . S2CID 1340468 .
•   Leino, K. Rustan M. (2001). „Rozszerzone sprawdzanie statyczne: perspektywa dziesięcioletnia”. Informatyka . Notatki z wykładów z informatyki. Tom. 2000. s. 157–175. doi : 10.1007/3-540-44577-3_11 . ISBN 978-3-540-41635-7 . {{ cite book }} : Brak lub pusty |title= ( pomoc )
• Detlefs, David L.; Leino, K. Rustan M.; Nelson, Greg; Saxe, James B. (1998). „Rozszerzone sprawdzanie statyczne”. Raport badawczy firmy Compaq SRC (159).