A data structure is called expressive, if the previous infinite disjunction is always first order definable. It turns out that standard arithmetic is expressive, whereas Presburger arithmetic is not. For expressive data structures, the Hoare calculus is relatively complete[3]. For a program C over an expressive data structure we therefore have :
