An input–output relational domain for algebraic data types and functional arrays

Der Artikel vertieft sich in die statische Analyse von Programmen, die mit algebraischen Datentypen (ADTs) und funktionalen Arrays umgehen, wobei der Schwerpunkt auf der kombinierten Analyse numerischer und ADT-Eigenschaften liegt. Es stellt eine neue, relationale abstrakte Domäne vor, die Beziehungen zwischen Werten nicht-rekursiver unveränderlicher ADTs und numerischer Eigenschaften ausdrückt. Diese Domäne kann mit verschiedenen numerischen relationalen Domänen instanziiert werden, was Flexibilität in der Präzision gegenüber anderen Domänen bietet. Kostenkompromisse. Der Artikel geht auch auf die Herausforderung ein, diese Analyse auf Programme mit funktionalen Arrays auszuweiten, eine detaillierte Konstruktion der abstrakten Domäne anzubieten und ihre Anwendung anhand eines motivierenden Beispiels zu veranschaulichen. Die Arbeit unterstreicht die Neuartigkeit der Kombination von relationaler Analyse mit funktionalen Arrays und ADTs und stellt einen bedeutenden Fortschritt im Bereich der statischen Analyse dar.