DoubleFormat.pvs 534 Bytes