Homework: Reading questions

Submit two items to the submission website (see link in the navigation bar at the top of the page):

Answer the following question:

Why does it not always work to define an abstraction function from code state to spec state in order to do a simulation proof that the code implements the spec? Assuming that the spec doesn’t make any premature decisions, what are two ways to extend the abstraction function idea so that it will always work?

The section in handout 6 labeled “Abstraction functions and simulation” and pages 4-6 in handout 8 are the most relevant.

Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.

Creative Commons License