[Question][Hw5] Abstract Semantics of Assign

[ShinWonho]

Hello, while implementing the HW5, I think there is a wrong description about abstract semantics of Assign

Here is the abstract semantics of Assign.
The integer abstraction of the result of eval is wrapped to the value abstraction and, it is updated to the memory.
However, the result of eval is not an integer abstraction any more.

As we can see, the result of eval is already a value abstraction.
Therefore, I think the abstract semantics should be just updating the value of x to the result of eval.

If there is any thing wrong, let me know.

Thank you!

[kangwoosukeq]

You're right. eval returns a value abstraction. I think it is our document problem. Sorry for the inconvenience.