Blame view

circus/help/development/development.html 8.6 KB
8d0dc533f   Madiel de Souza Conserva Filho   first
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
  <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">
          Desenvolvimento
        </td>
      </tr>
      <tr>
        <td class="grande" width="500">
          <br>
                 <div align="justify">  Após a especificação original ter sido carregada,
                 iniciamos a etapa de refinamento. Assim, partimos de uma especificação abstrata, geralmente centralizada,
                 e através de sucessivas aplicações de leis de refinamento, passamos para um estado
                 concreto, possivelmente distribuída.
                 <br>
  
                 <h5>Aplicando Lei</h5>
                   Para aplicarmos uma lei, devemos selecionar um termo específico. Essa seleção
                  é realizada sobre as linhas da janela <a href="../gui/development.html" target="body">
                  Desenvolvimento</a>; segure a tecla CTRL e clique na primeira e na última linha para selecionar múltiplas linhas.
  
                  <br>
                  <br>
                  <img border = "0" src="../images/selection.jpg" align="center">
                  <br>
                  <br>
  
                   Uma vez selecionado o termo, a ferramenta nos permite verificar através do Popup Menu, quais
                  leis são aplicáveis àquele termo. Para visualizar o PopUp Menu, clique no botão da direita sobre a seleção na
                  janela de Desenvolvimento. Caso exista alguma lei aplicável ao termo selecionado, as linhas que determinam esse termo
                  serão todas selecionadas.
  
                  <br>
                    Para selecionarmos e aplicarmos uma lei devemos, Devemos ir no Menu de "Aplicar Lei" e selecionar a lei desejada.
  
                  <br>
                  <br>
                  <img border = "0" src="../images/selectionlaw.jpg" align="center">
                  <br>
                  <br>
  
                   Também podemos selecionar a lei, através do Textfield presente no
                  Toolbar da janela principal. Para isto devemos clicar com o botão esquerdo
                  no mesmo.
  
                  <br>
                  <br>
                  <img border = "0" src="../images/selectionlaw2.jpg" align="center">
                  <br>
                  <br>
  
                   Ao clicarmos no mesmo, um PopUp Menu de leis, será exibido. Tal menu contém
                  uma classificação de leis que facilitam a sua seleção, dado a grande quantidade
                  de leis. 
  
                  <br>
                  <br>
                  <img border = "0" src="../images/selectionlaw3.jpg" align="center">
                  <br>
                  <br>
  
                   Após a devida lei ser selecionada, o TextField guardará o nome da lei.
                  No caso dessa lei ser aplicável ao termo selecionado, o botão de <img border =
                  "0" src="../../../images/generate.gif" align="center">
                  será habilitado, permitindo que haja aplicação da lei selecionada.
  
                  <br>
                  <br>
                  <img border = "0" src="../images/butaoapply.jpg" align="center">
                  <br>
                  <br>
  
                   A aplicação da lei poderá ser efetuada tanto pelo clique no botão de aplicação de lei, 
                   quanto pela opção de aplicar lei referente ao Popup Menu associado ao TextField. Para visualizarmos
                  tal Popup Menu, devemos clicar com o botão direito no TextField. Caso o termo selecionado
                  unifique o termo que a lei é aplicável, as linhas referentes a esse termo são todas
                  selecionadas e a opção de "Aplicar Lei" é habilitada. Tal Popup Menu também apresenta uma opção para
                  ver os <a href="../utils/law-details.html" target="body"> Detalhes da Lei</a>
  
                  <br>
                  <br>
                  <img border = "0" src="../images/applyLaw.jpg" align="center">
                  <br>
                  <br>
  
  
                   Algumas leis necessitam que certos argumentos sejam passados como
                  parâmetros. Para cada argumento uma pequena janela é exibida para que o
                  usuário passe o mesmo. Inicialmente a janela está habilitada para receber
                  um argumento passado no formato LaTeX.
  
                  <br>
                  <br>
                  <img border = "0" src="../images/param.jpg" align="center">
                  <br>
                  <br>
  
                   No entanto, o argumento também poderá ser digitado em Unicode,
                  o usuário deverá apenas setar a opção de Unicode no ComboBox da janela
                  Parâmetro. A inserção de símbolos Unicode é realizada através do <a href=
                  "../utils/virtual-keyboard.html" target="body"> Teclado Virtual</a>
  
                  <br>
  
                   Depois que os argumentos necessários são passados, a aplicação da
                  lei é concluída. Nesse momento, as janelas Desenvolvimento e <a href=
                  "../gui/code.html" target="body"> Código</a> são atualizadas. A janela
                  <a href="../gui/proofobligation.html" target="body"> Obrigação de Prova</a>
                  também pode ser atualizada caso a aplicação de lei gere alguma obrigação de
                  prova. Ao final da janela de <a href="../gui/development.html" target="body">
                  Desenvolvimento</a>, o nome da lei que foi aplicada é exibida, junto do tipo
                  de aplicação de lei: simulação, refinamento ou equivalência. Através da seleção
                  dessa da linha que contém a aplicação de lei e do Popup Menu associado a janela de
                  Desenvolvimento, podemos ver os <a href="../utils/law-details.html" target="body">
                  Detalhes da Lei.</a> Em seguida, o termo que a lei gera é exibido ao final do
                  refinamento.
  
                  <br>
                  <br>
                  <img border = "0" src="../images/lawapply.jpg" align="center">
                  <br>
                  <br>
  
                  <br>
                  <h5>Coletando Código</h5>
  
                   Eventualmente, para aplicarmos certas leis a alguns termos cujos filhos
                  foram alvos de aplicações de leis, devemos capturar a nova instância desses termos.
                  Tal atividade é realizada através de uma Coleta de Código. Tal coleta é baseada
                  em dois tipos de termos: Acoes e Processos.
                  <br>
                   Para realizarmos uma Coleta de Código devemos primeiramente selecionar o tipo
                  de coleta, ou seja, Coleta de Ação ou Coleta de Processo. Para isto, seleciona-se
                  o tipo desejado no primeiro ComboBox pertecente ao ToolBar da janela Principal do
                  CRefine.
  
                  <br>
                  <br>
                  <img border = "0" src="../images/optionsCollect.jpg" align="center">
                  <br>
                  <br>
  
                   Após ter selecionado o tipo de Coleta de Código, o segundo ComboBox será
                  atualizado de acordo com o tipo de coleta que foi selecionado e as novas instâncias
                  da categoria de termos selecionada, estarão disponíveis para serem coletadas através
                  da seleção de seus nomes no segundo ComboBox do ToolBar da janela Principal.
  
                  <br>
                  <br>
                  <img border = "0" src="../images/collectTerm.jpg" align="center">
                  <br>
                  <br>
  
                   Logo após a seleção do termo que será coletado ser efetuada, apenas a janela
                  de Desenvolvimento sofrerá alteração. Ela apresentará uma indicação que houve Coleta
                  de Código e logicamente, exibirá o termo coletado ao final do refinamento.
  
                  <br>
                  <br>
                  <img border = "0" src="../images/collectedTerm.jpg" align="center">
                  <br>
                  <br>
  
                   Outra forma de se realizar uma coleta de Código é através do Popup Menu associado
                  a janela Desenvolvimento. Pela opção "Coletar Código" do mesmo, podemos selecionar a
                  a categoria de termo que será coletado: Ação ou Processo. E a partir do mesmo, seleciona-se
                  o termo desejado.
  
                  <br>
                  <br>
                  <img border = "0" src="../images/collectTerm2.jpg" align="center">
                  <br>
                  <br>
  
                  </div>
        </td>
      </tr>
  </table>
  
  
  </body>
  
  </html>