On Refinement Calculus with Program Window Inference

摘要

Data refinement is hard to deal with in a refinement tool than ordinary algorithmic refinement, since data refinement usually has to be done on a large program component at once. In the paper, firstly, the badkground is introduced, then the data refinement calculator is constructed. At last we argue an approach for data refinement which is based on data refinement calculus nand program window inference.