data specification using ownership IdxO[A] = . × .(. id : Id;. O : Ref[A] → Id) ; variables idxO : IdxO[A]; of : Ref[A] → Id; id : Id; end data specification