Juliano Cardoso / circusRefine

proofobligation.html 4.13 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
  74
  75
  76
  77
  78
  79
  80
  81
  82
  83
  84
  85
  86
  87
  88
  89
  90
  91
  92
  93
  94
  95
  96
  97
  98
  99
 100
<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">
        Proof Obligations
      </td>
    </tr>
    <tr>
      <td class="grande" width= "500">
        <br>
        <div align="justify">
        Some law applications may require the satisfaction of certains condition under which the law
        application is valid. The proof obligations generated during the development are shown in
        the Proof Obligations window.  

        <br>
        After being generated, the proof obilgations are given to the theorem prover that tries to 
        verify the validity of the condition. Currently, this theorem prover is internal to CRefine and small; it 
        verifies only some of the syntactic restrictions. For this reason, a status is given to each proof obligation.
        This status can be:
         <img border = "0" src="../../../images/true.gif" align="center"> (true),
        <img border =
                "0" src="../../../images/false.gif" align="center"> (false),
        <img border =
                "0" src="../../../images/inter.gif" align="center"> (undetermined),
        <img border = "0" src="../../../images/maotrue.gif" align="center"> (manually proven true) and <img border = "0" src="../../../images/maofalse.gif" align="center"> (manually proven false).

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

        <br>
        by selecting the proof obligation, the line in the development window that corresponds to
        the law application that generated the proof obligation is highlighted.

        <br>

        An important functionality, offered by CRefine's current theorem proving facilities, is to give
        to the user the choice of seeing the proof obligations in its expanded format using the definitions
        of the syntactic functions. In order to see the expanded or contracted version of the proof obligations,
        the user must select the proof obligation and click on the right button of the mouse: a pop-up menu
        is shown to the user. Using this pop-up menu, we have access to three important functionalities: manual proof, edit, and show. 

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

        The manual proof allows the user to define the proof obligation status for those proof obligations
        that could not be proved by CRefine theorem proving facilities. As the name suggests, these proofs must
        have been manually done by the user. After setting the status of a proof obligation, the proof obligation window is updated accordingly.
        The action of setting a status for proof obligations can also be undone/redone.

        <br>
        
        Another functionality is the exhibition of proof obligations in either expanded or contracted format.
        The latter is the standard format. The former applies the definitions of the syntactic functions to show
        the calculated predicates. For this reason, only those proof obligations with syntactic functions on it
        can be exanded/contracted. In order to select the format, start the pop-up menu of the proof obligation 
        window and select "Show -> Expanded". Analogously, we have the "Show -> Contracted" option. 

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

        After choosing the new format the proof obligation is shown in the desired format. This action can also be undone/redone.

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

        The functionality of copying the text of a proof obligation to the system clipboard is describe in <a href=
        "../utils/copy.html" target="body">Copy</a>.
        </div>
      </td>
    </tr>
</table>

</body>

</html>