SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Quantifying over Elements of a Container

by Claire Dross in Formal Verification – May 17, 2016

Containers holding several items of the same type such as arrays, lists, or sets are a common occurrence in computer programs. Stating a property over such containers often involves quantifying over the elements they contain. The way quantified formulas over containers are translated for proof can be tuned in GNATprove using a specific annotation.