search

m-carrasco / TinyBCT

MIT License
3 stars 2 forks source link

Create flag to assume closed world with respect to classes #28

Closed m-carrasco closed 6 years ago

m-carrasco commented 6 years ago

Currently subtyping axioms allow classes not present in the dll to exist. Another possibility would be to assume that only existing classes can occur.

rcastano commented 6 years ago

I'm working on a quick hack (replacing the "assert false" with a havoc. But this could lead to false negatives with respect to exceptions. We need to add assumptions for each existing type Base and existing subtypes A, B, C such that forall T subtype(T, Base) implies T == A || T == B || T == C. This is also related to the following documented shortcoming (should pass, but fails assertion). We might need to update the test after the hack too.

https://github.com/m7nu3l/TinyBCT/blob/0841ed8eb96977740b6afc94f48619c7bb037a2a/Test/DynamicDispatch.cs#L309-L327

Code tested in the following test: https://github.com/m7nu3l/TinyBCT/blob/0841ed8eb96977740b6afc94f48619c7bb037a2a/TinyBCT/Tests/Tests.cs#L1302-L1308

rcastano commented 6 years ago

I have trouble testing and believe there are interactions with issue #33. Work on this issue on hold for the moment.

rcastano commented 6 years ago

We decided against adding this flag. We realized it was not necessary and that the unwanted behaviors we were seeing were due to bugs which were fixed within issue #29.