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.
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.
Para selecionarmos e aplicarmos uma lei devemos, Devemos ir no Menu de "Aplicar Lei" e selecionar a lei desejada.
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.
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.
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
será habilitado, permitindo que haja aplicação da lei selecionada.
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 Detalhes da Lei
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.
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 Teclado Virtual
Depois que os argumentos necessários são passados, a aplicação da lei é concluída. Nesse momento, as janelas Desenvolvimento e Código são atualizadas. A janela Obrigação de Prova também pode ser atualizada caso a aplicação de lei gere alguma obrigação de prova. Ao final da janela de Desenvolvimento, 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 Detalhes da Lei. Em seguida, o termo que a lei gera é exibido ao final do refinamento.
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.
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.
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.
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.
Aplicando Lei
Para aplicarmos uma lei, devemos selecionar um termo específico. Essa seleção é realizada sobre as linhas da janela Desenvolvimento; segure a tecla CTRL e clique na primeira e na última linha para selecionar múltiplas linhas.
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.
Para selecionarmos e aplicarmos uma lei devemos, Devemos ir no Menu de "Aplicar Lei" e selecionar a lei desejada.
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.
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.
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
será habilitado, permitindo que haja aplicação da lei selecionada.
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 Detalhes da Lei
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.
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 Teclado Virtual
Depois que os argumentos necessários são passados, a aplicação da lei é concluída. Nesse momento, as janelas Desenvolvimento e Código são atualizadas. A janela Obrigação de Prova também pode ser atualizada caso a aplicação de lei gere alguma obrigação de prova. Ao final da janela de Desenvolvimento, 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 Detalhes da Lei. Em seguida, o termo que a lei gera é exibido ao final do refinamento.
Coletando Código
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.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.
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.
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.
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.