Juliano Cardoso / circusRefine

doc-generator.html 2.18 KB
edit raw blame history 
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
<html>
<head>
    <title>CRefine</title>
    <link rel="stylesheet" type="text/css" href="../../style.css" />

</head>

<body>

<table>
    <tr height="10">
      <td>
      </td>
    </tr>
    <tr>
      <td class="tituloAzul">
        Document Generator
      </td>
    </tr>
    <tr>
      <td class="grande" width="500">
        <br>
        <div align="justify">
        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.
        <br>
        In order to generate the output file we can click on the button <img border = "0" src="../../../images/print.gif" align="center">
        or choose the Print option in the Development menu.

        <br>
        <br>
        <img border = "0" src="../images/doc.jpg" align="center">
        <br>
        <br>
        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.

        <br>
        <br>
        <img border = "0" src="../images/doc2.jpg" align="center">
        <br>
        <br>

        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.
        <br>
        <br>
        <img border = "0" src="../images/doc3.jpg" align="center">
        <br>
        <br>
        A message will be given at the end of the generation.
        <br>
        <br>
        <img border = "0" src="../images/doc4.jpg" align="center">
        <br>
        <br>


        </div>
      </td>
    </tr>
</table>


</body>

</html>