Thank you Jaak and Stephan. I was also thinking about functional representation, but purposely chosen sets to closely model SQL, because access by index is not the only access I need to verify. I probably can create wrapper functions/operators to make it look functional, or re-think my approach again.
Yuri
P.S. Jaak, regarding your comment about using id \in DOMAIN theSet. It is also possible to use a slightly different approach: theSet[id] = NoVal if id \in SomeSet and you initialize theSet = [p \in SomeSet |-> NoVal] as described in Specifying Systems on p 52.