the algorithm is a bit less strict than Liberty Eiffel's
ensure
Result /= Void implies Result.image.count >= 2 and then Result.image.first = '"' or else Result.image.count >= 3 and then Result.image.first = 'U' and then Result.image.item(2) = '"' and then Result.image.last = '"'