Review

class Util {
   /*@ requires 0 <= offset && offset < length;
     @ requires 0 <= length && length <= in.length;
    */
   public static byte[] pad(/*@ non_null */ byte[] in,
                            int offset, int length) {
      ByteArrayOutputStream out = new ByteArrayOutputStream();
      out.write(in, offset, length);
      out.write((byte)0x80);
      while (out.size() % 8 != 0) {
        out.write((byte)0x00);
      }
      return out.toByteArray();
   }

}