data specification using nat wlstatus := used | free | erroneous | erasing ; variables stat : wlstatus; end data specification