marcoeilers / nagini

Nagini is a static verifier for Python 3, based on the Viper verification infrastructure.
Mozilla Public License 2.0
233 stars 8 forks source link

Fixing union subtype axiom #197

Closed marcoeilers closed 5 months ago

marcoeilers commented 5 months ago

Turns out it's not true for all types T1, T2, T3 that T1 <: Union[T2, T3] iff T1 <: T2 or T1 <: T3. If T1 is itself a union type it's not necessary that the entire union T1 is a subtype of either T2 or T3, this just has to be true for all of its components.

Also, we add the assumption that no object's actual runtime type is a union type.

This fixes #196.


This change is Reviewable