data specification using wlstatus wlentry := wl-entry(. .ec : nat;. .status : wlstatus) ; variables wle : wlentry; end data specification