Blame view
circus/help/development/development.html
8.6 KB
8d0dc533f
![]() |
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> |