Abstract:Data refinement is hard to deal with in a refinement tool compared with ordinary algorithmic refinement, since data refinement usually has to be done on a large program component at once. So it is important to learn how to perform data refinement effectively. In this paper, the background is introduced first, then the data refinement calculator is constructed. Finally an approach is proposed for data refinement which is based on data refinement calculus and program window inference.