The ref package

routines for refinement checking between modules

By Sriram Rajamani

This package has routines that check if one module refines another. 1. refinement check is provided via the check_refine command. It requires that all history dependent variables of the specification be witnessed in the implementation 2. simulation check is provided via the check_simulate command. 3. compositonal refinement facility is provided by the check_refine_atom command. This command helps the user carry out one proof oligation in a compositional proof.
Last updated on 980624 22h11