specification sorts volid; variables v : volid; v0 : volid; v1 : volid; v2 : volid; end specification