Using Type Extension to Organize Virtual Memory Mechanisms.

摘要

Much effort is being devoted to producing computer systems that are easy to understand, verify, and develop. The general methodology for designing such systems consists of organizing each system into a set of modules so that the module can be understood, verified, and developed individually, and so that the understanding and verification of the system can be derived from the understanding and verification of its modules. While many of the mechanisms in computer systems have been successfully structured into sets of modules, no technique has been proposed to organize the virtual memory mechanism of a system in such a way. This thesis proposes to use type extension for that purpose.