search

overturetool / overture

The Overture Tool
http://overturetool.org
GNU General Public License v3.0
49 stars 25 forks source link

Add InvariantValueMaps from VDMJ #770

Closed nickbattle closed 3 years ago

nickbattle commented 3 years ago

Several problems have been seen with named types that include either "eq" or "ord" clauses, and maps of these. The problem is that if the "eq" clause does not match the equals/hashCode contract in Java (and there is no reason why it should) then a HashMap will produce errors. This was solved by moving to TreeMaps that use compareTo rather than hashCode/equals in Java, but of course this can be upset by "ord" clauses that do not match the compareTo Java contract.

The solution in VDMJ is to introduce a new InvariantValueMap class that works purely using Java equals (not hashCode). A normal ValueMap uses a HashMap, and if anything is added to the domain of the map that defines an "eq" clause, then the ValueMap delegates to an InvariantValueMap (this dynamic choice is for performance, since the InvariantValueMap isn't very efficient without hashCodes).

This issue is used to port the same change into Overture.

nickbattle commented 3 years ago

Fix is now available in ncb/development.