CIL code also generates constraints over types. The current expression system should be extended to formulate such constraints and the solver to decide them.
The constraints should be able to generate a new type. For code like bellow, the type constraints for the variable o in order to pass the second condition are (class TO : IBar2, IBar3, IBar4) && !(class TO : IBar1).
int Foo(object o)
{
if (o is IBar1) return 1;
else if (o is IBar2 && o is IBar3 && o is IBar4) return 2;
else return 3;
}
The type itself may be a symbol - symbolic type. The system should handle inheritance and polymorphism. Can the Theory of DataTypes be applied? The type system is directed acyclic graph...
CIL code also generates constraints over types. The current expression system should be extended to formulate such constraints and the solver to decide them.
The constraints should be able to generate a new type. For code like bellow, the type constraints for the variable
oin order to pass the second condition are(class TO : IBar2, IBar3, IBar4) && !(class TO : IBar1).The type itself may be a symbol - symbolic type. The system should handle inheritance and polymorphism. Can the Theory of DataTypes be applied? The type system is directed acyclic graph...