PR# 15938 Bad postcondition in {EV_ANY}.set_data

The postcondition does not hold in the case where the data item is a DOUBLE or REAL.

It should read:

data_assigned: (some_data = some_data) implies (data = some_data)

When I say we didn't have time now, I should have been more precise and mentionned that 6.4 was already frozen for the release which will happen in the next couple of days.

To include the fix in 6.5, please send us a patch and we will review it and most likely integrate it if we agree.

I'm leaving the bug suspended because this issue is more complex than just EV_ANY.

That doesn't interest me. I want to change the source code repository so the fix will flow through when 6.4 is released.

You can certainly do the changes in your local copy of Vision2.

Well, if you don't have the time to make these changes, may I do so?

It is unlikely that we will change this in the near future since there are more important things to fixed than vision2 in this area. However to solve the short term issue you are having, you could do this instead:

v2.set_data (create {CELL [DOUBLE]}.put (d))

and this will not violate the postcondition of `set_data'.

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).