static public Header header(byte[] buf) {
        String format;        
        try {
            format = new String(buf, 0, 4, StandardCharsets.US_ASCII);   
        } catch (RuntimeException err) {
            throw new Error("Error parsing format", err);
        }
        int version;
        switch (format) {
            case "WDBC": {
                version = 1; 
                break;    
            }
            case "WDB2": {
                version = 2; 
                break;
            }
            default: 
                throw new Error("Unknown format: " + format, null);
        }
        ByteBuffer bb = ByteBuffer.wrap(buf).order(ByteOrder.LITTLE_ENDIAN);
        try {
            int rowCount = bb.getInt(4);
            int colCount = bb.getInt(8);
            int rowSize = bb.getInt(12);
            //int strSize = bb.getInt(16);
            int row0;
            if (version == 2) {
                final int H = 48;
                int id0 = bb.getInt(32);
                int id1 = bb.getInt(36);
                if (id1 != 0) {
                    row0 = H + (1 + id1 - id0) * 6;
                } else {
                    row0 = H;
                }
                //byte[] v = Arrays.copyOfRange(buf, H,  row0);
                //System.out.println(Arrays.toString(v));
            } else {
                row0 = 20;
            }       
            return new Header(format, rowCount, colCount, rowSize, row0);
        } catch (RuntimeException err) {
            throw new Error("Error parsing header", err);
        }
    }