Uitgebreide statische controle - Extended static checking

Uitgebreide statische controle ( ESC ) is een verzamelnaam in de informatica voor een reeks technieken voor het statisch controleren van de juistheid van verschillende programmabeperkingen. ESC kan worden gezien als een uitgebreide vorm van typecontrole . Net als bij typecontrole wordt ESC automatisch uitgevoerd tijdens het compileren (dwz zonder menselijke tussenkomst). Dit onderscheidt het van meer algemene benaderingen van de formele verificatie van software, die doorgaans afhankelijk zijn van door mensen gegenereerde bewijzen. Bovendien bevordert het de bruikbaarheid boven degelijkheid, in die zin dat het tot doel heeft het aantal valse positieven (overschatte fouten die geen echte fouten zijn, dat wil zeggen ESC boven striktheid) drastisch te verminderen ten koste van het introduceren van enkele valse negatieven (echte ESC-onderschattingsfout, maar die geen aandacht van de programmeur nodig hebben, of die niet het doelwit zijn van ESC). ESC kan een reeks fouten identificeren die momenteel buiten het bereik van een typecontrole vallen, waaronder delen door nul , array-out-of-bounds , integer-overflow en null-dereferenties .

De technieken die bij uitgebreide statische controle worden gebruikt, zijn afkomstig uit verschillende gebieden van de computerwetenschappen , waaronder statische programma-analyse , symbolische simulatie , modelcontrole , abstracte interpretatie , SAT-oplossing en geautomatiseerd bewijs van stellingen en typecontrole . Uitgebreide statische controle wordt over het algemeen alleen uitgevoerd op een intraprocedureel niveau (in plaats van een interprocedureel niveau) om op te schalen naar grote programma's. Verder is uitgebreide statische controle bedoeld om fouten te rapporteren door gebruik te maken van door de gebruiker aangeleverde specificaties, in de vorm van pre- en postcondities , lusinvarianten en klasse-invarianten .

Uitgebreide statische checkers werken doorgaans door de sterkste postcondities (resp. zwakste precondities ) intraprocedureel te verspreiden via een methode die uitgaat van de preconditie (resp. postconditie). Op elk punt tijdens dit proces wordt een tussenvoorwaarde gegenereerd die vastlegt wat op dat programmapunt bekend is. Dit wordt gecombineerd met de noodzakelijke voorwaarden van de programmaverklaring op dat moment om een verificatievoorwaarde te vormen . Een voorbeeld hiervan is een uitspraak met betrekking tot een deling, waarvan de noodzakelijke voorwaarde is dat de deler niet nul is. De verificatievoorwaarde die hieruit voortvloeit, luidt feitelijk: gegeven de tussenvoorwaarde op dit punt, moet volgen dat de deler niet nul is . Aangetoond moet worden dat alle verificatievoorwaarden onwaar zijn (dus correct door middel van uitgesloten derde ) om een ​​methode te laten slagen voor uitgebreide statische controle (of "niet in staat om meer fouten te vinden"). Meestal wordt een of andere vorm van geautomatiseerde stellingbewijzer gebruikt om verificatievoorwaarden te ontladen.

Extended Static Checking werd ontwikkeld in ESC/Modula-3 en later in ESC/Java . De wortels zijn afkomstig van meer simplistische statische controletechnieken, zoals statische debugging of Lint (software) en FindBugs . Een aantal andere talen hebben ESC overgenomen, waaronder Spec# en SPARKada en VHDL VSPEC. Er is momenteel echter geen veelgebruikte programmeertaal voor software die uitgebreide statische controle biedt in de basisontwikkelomgeving.

Zie ook

• Java-modelleringstaal (JML)

Referenties

Verder lezen

• Cormac Flanagan; K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata (2002). Uitgebreide statische controle voor Java . Proceedings of the Conference on Programming Language Design and Implementation (PLDI) . P. 234. doi : 10.1145/512529.512558 . ISBN 978-1581134636.CS1 maint: meerdere namen: auteurslijst ( link )
• Babic, Domagoj; Hu, Alan J. (2008). Calysto: schaalbare en nauwkeurige uitgebreide statische controle . Proceedings van de International Conference on Software Engineering (ICSE) . P. 211. doi : 10.1145/1368088.1368118 . ISBN 9781605580791.
• Schaken, BV (2002). Verbetering van de computerbeveiliging met behulp van uitgebreide statische controle . Proceedings of IEEE Symposium on Security and Privacy . blz. 160-173. CiteSeerX  10.1.1.15.2090 . doi : 10.1109/SECPRI.2002.1004369 . ISBN 978-0-7695-1543-4.
• Rioux, Frederic; Chalin, Patrice (2006). "De kwaliteit van webgebaseerde bedrijfsapplicaties verbeteren met uitgebreide statische controle: een case study" . Elektronische notities in theoretische informatica . 157 (2): 119-132. doi : 10.1016/j.entcs.2005.12.050 . ISSN  1571-0661 .
• James, Perry R.; Chalin, Patrice (2009). "Sneller en completer uitgebreide statische controle voor de Java-modelleringstaal". Tijdschrift voor automatisch redeneren . 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). Uitgebreide statische controle op haskell . Proceedings van de ACM Workshop over Haskell . P. 48. CiteSeerX  10.1.1.377.3777 . doi : 10.1145/1159842.1159849 . ISBN 978-1595934895.
• Leino, K. Rustan M. (2001). Uitgebreide statische controle: een perspectief van tien jaar . Informatica . Collegenota's in de informatica. 2000 . blz. 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; Saksen, James B. (1998). "Uitgebreide statische controle". Compaq SRC-onderzoeksrapport (159).