# Invariants for global variables

 Hare Nov 30, 2012 at 12:24 PM Hi, I'm considering is it possible to state the invariants for global variables? Which may specify the properties for the variables like in structure. And if I have a field in a struct, is that possible for me to bind it to a field in another struct? For example in following code. I have a struct T and I'd like to specify that the value of s_val[t] is equal to t->val? And also is that possible to say that s_sortedarr[] is sorted with invariant? typedef struct T{ unsigned val; }T; T *px; _(ghost struct { // other fields of the struct unsigned s_val[T*]; unsigned s_sortedarr[]; };)  Thanks very much! Shu Cheng erniecohen Developer Dec 5, 2012 at 1:24 PM Hi Shu, - If you want to add an invariant constraining the nonvolatile fields of a particular object such as px of some type, you put those invariants in another object that knows that px is closed (typically because it transitively owns px). - Global variables of primitive types are fields of anonymous global objects (one per variable, obtainable through \embedding()). Thus, if you want to talk about fields of *px, you want to own both \embedding(&px) (the object that owns the variable px) and px (the T that px points to). The natural choice in your example is the global ghost object (lets call it s). - Before using these globals, they have to be initialized and wrapped up. This requires someone to start out with ownership of them; the only place to "get" this ownership is at program entry. Here is a solution putting these together: typedef struct T{ unsigned val; }T; T *px; _(ghost struct { // other fields of the struct unsigned s_val[T*]; unsigned s_sortedarr[]; _(invariant \mine(\embedding(&px))) _(invariant \mine(px)) _(invariant px->val == s_val[px]) } s;) void main() _(requires \program_entry_point()) _(writes &px, \embedding(&px), \extent(&s)) { px = malloc(sizeof(T)); _(assume px) px->val = 0; _(wrap px) _(wrap \embedding(&px)) _(ghost s.s_val = \lambda T *t; (unsigned) 0) _(wrap &s) // invariants established - start using s/px }  Hope this helps, ernie Hare Dec 7, 2012 at 2:33 PM Hi Ernie, This is quite helpful for me. Thanks very much!!