An additional postcondition would also be useful:

not_a_number: (some_data /= some_data) implies (data /= data)

(I don't know how good the assertion label is - I have only ever encountered these situations with NaNs, so I think it is reasonable).