CRefine

Document Generator

CRefine allows users to produce a final file in .tex format that contains all the refinement steps, as well as the proof obligations, the comments, and the final code. The comments can be included in the final file before the line it has be inserted or a list of comments at the end of the file. This output file cab be used in the generation of a pdf file that provides an excellent visualisation of the overall refinement.
In order to generate the output file we can click on the button or choose the Print option in the Development menu.
After selecting Print, a window is shown the user. Using this window, the user must select the development items that must be part of the output file. The user can also choose the format in which the proof obligation must be included: expanded or contracted.
After confirming the selection by clicking on "OK", a dialog box is shown: the user must select the location of the output file and its name. The generated file will be in LaTeX format.
A message will be given at the end of the generation.