NYET--attempted formal specs (again)