Syftet med statisk analys är att härleda invarianter om program som är tillräckligt exakta för att etablera semantiska egenskaper, såsom frånvaron av run-time fel. I stort sett finns det två huvudgrenar av statisk analys för tvingande program. Pekar- och formanalyser fokuserar på infererande egenskaper hos pekare, dynamiskt fördelade minne och rekursiva datastrukturer, medan numeriska analyser försöker härleda invarianter på numeriska värden. Även om det ofta behövs samtidiga slutsatser av formämnen, är detta fall särskilt utmanande och inte särskilt väl utforskat. Särskilt, samtidig form-numerisk slutsats väcker komplexa frågor i utformningen av den statiska analysatorn själv. I detta papper studerar vi konstruktionen av sådana form-numeriska, statiska analysatorer. Vi sätter upp en abstrakt tolkningsram som gör att vi kan resonera om samtidiga form-numeriska egenskaper genom att kombinera form och numeriska abstraktioner till en modulär, uttrycksfull abstrakt domän. En sådan modulstruktur är mycket önskvärd för att göra dess formalisering och genomförande lättare att göra och få rätt. För att uppnå detta väljer vi en konkret semantik som kan abstrakteras steg för steg, samtidigt som vi bevarar en hög expressivitetsnivå. Den abstrakta verksamhetens struktur (dvs. överföring, förening och jämförelse) följer strukturen i denna semantik. Fördelen med denna konstruktion är att dela analysatorn i moduler och functors som implementerar abstraktioner av olika funktioner.
En modulär kombination av form och numeriska domäner har föreslagits i REF.
Modular Construction of Shape-Numeric Analyzers
{'venue': 'EPTCS 129, 2013, pp. 161-185', 'journal': None, 'mag_field_of_study': ['Computer Science']}