search

prosyslab-classroom / cs424-program-reasoning

44 stars 16 forks source link

[Question][Hw2] #155

Closed 08kmc09 closed 3 months ago

08kmc09 commented 1 year ago

Name: Mincheol Kwon

YOUR QUESTION

src_x = tgt_x /\ src_y + 0 = src_x /\ not (src_y = tgt_x)

In the README.md, the explanation of Program Equivalence Checker is defined as above.

However, I think it should be replaced with src_x = tgt_x /\ src_y = src_x + 0 /\ not (src_y = tgt_x)

I think the intentional derivation was functional congruence. So the body part calculation is misleading.

goodtaeeun commented 12 months ago

I am sorry for the late reply. Thank you for suggesting a correction for the homework description.

You are correct. src_x = tgt_x /\ src_y = src_x + 0 /\ not (src_y = tgt_x) will be the right formula for the given example.