prosyslab-classroom / is593-language-based-security

28 stars 6 forks source link

[Homework 4] Narrowing operator for values #17

Closed KunJeong closed 4 years ago

KunJeong commented 4 years ago

Hi again. Currently, the PowSet functor returns a failure with the narrowing operator. In the case of Sign domain that doesn't support narrowing, we can just widen and terminate and not narrow at all, but for Interval domain that is not possible. Since a value contains Numerical, LocSet and FunSet, how can I define a proper narrowing operator for Values? Thank you.

KihongHeo commented 4 years ago

As we define widen for Sign as join, you can define narrow for the power-set domains as meet (i.e., set intersection).

KunJeong commented 4 years ago

Aha. Then I guess it would be better to replace the fail with "Unsupported" with meet instead?

KihongHeo commented 4 years ago

Yes. But in the homework, two arguments of the narrow will have always the same value because no widening for power-set is applied.

KunJeong commented 4 years ago

Hmm. I still don't see why this is the case. Isn't the two arguments of narrow generally the input and output of the abstract semantic function? How are these the same?

KihongHeo commented 4 years ago

(answer changed) You are right. Ignore the comment. Just meet for narrow is enough.

KunJeong commented 4 years ago

Oh I saw the change just now. Thank you.