<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">
Development
</td>
</tr>
<tr>
<td class="grande">
<div align="justify">
After loading the original specification, we start the development stage.
So, we start from the abstract specification, which is generally centralised,
and using successive refinement law applications, we reach the concrete specification,
which is generally distributed.
<br>
<h5>Applying Refinement Laws</h5>
In order to apply a refinement law, we must select a specific term. This selection is
realised on the lines of the <a href="../gui/development.html" target="body">
development window</a>; hold the CTRL key and click on the first and last line of the term
in order to select multiple lines.
<br>
<br>
<img border = "0" src="../images/selection.jpg" align="center">
<br>
<br>
Once you have selected a term, the tool allows us to check, using a pop-up menu, which laws can
be applied to the selected term. Using the right button, click on the selected term to visualise the pop-up menu.
If there are any refinement law that can be applied to the selected term, the names of these laws will be displayed.
<br>
Go to "Apply Law" on the menu and select the desired law in the pop-up menu if you wish to apply the law.
<br>
<br>
<img border = "0" src="../images/selectionlaw.jpg" align="center">
<br>
<br>
We can also selected a law to apply using the text field in the right-hand side
of the toolbar in the main window. For that, click, using the left button, on it.
<br>
<br>
<img border = "0" src="../images/selectionlaw2.jpg" align="center">
<br>
<br>
After clicking on it, a pop-up menu of laws will be displayed. This menu classifies
the laws; this facilitates their selection, given the large number of existent laws.
<br>
<br>
<img border = "0" src="../images/selectionlaw3.jpg" align="center">
<br>
<br>
After selecting the law, the text field will store the law name. If the law is applicable to
the selected term, the button <img border =
"0" src="../../../images/generate.gif" align="center">
will be enabled. Hence, the law may be applied.
<br>
<br>
<img border = "0" src="../images/butaoapply.jpg" align="center">
<br>
<br>
The law application can be done either by clicking on the apply law button or by choosing
the apply law option in the pop-up menu that can be activated from the text field. In order to visualise
this pop-up menu, we must click, using the right button, on the text field. If the selected term pattern matches with
the law, the lines of the term will be highlighted and the apply law option will be enabled. This pop-up menu has also
a see <a href="../utils/law-details.html" target="body">Law details</a> option.
<br>
<br>
<img border = "0" src="../images/applyLaw.jpg" align="center">
<br>
<br>
Some laws are parametrised and need that some arguments are given to them before their application.
For each argument, a small window will be displayed and can be used to input the right argument. Initially,
this window is set to receive arguments in the LaTeX format.
<br>
<br>
<img border = "0" src="../images/param.jpg" align="center">
<br>
<br>
However, the argument can also be given in Unicode format, the user only need to set
this option using the Combo box in the parameter window. The insertion of symbols in Unicode
format can be done using the <a href=
"../utils/virtual-keyboard.html" target="body"> Virtual Keyboard</a>.
<br>
After giving the arguments, the law application takes place. In this moment, the Development
and <a href=
"../gui/code.html" target="body"> Code </a> window are updated. The
<a href="../gui/proofobligation.html" target="body">Proof Obligation</a> window may also be updated
if the law application generates any new one. The development windows is updated with
a new line that contains the name of the law that was applied and the type of refinement (simulation, refinement, or equivalence), and the resulting term.
By selecting the line that contains the law name, and starting the pop-up menu, we may
see the <a href="../utils/law-details.html" target="body">
Law Details</a>.
<br>
<br>
<img border = "0" src="../images/lawapply.jpg" align="center">
<br>
<br>
<br>
<h5>Collecting Code</h5>
Eventually, the application of laws to terms whose sons have already been modified, requires
the exhibition of a new instance of the whole term. This is called Term Collection. This collection is
based on two kinds of terms: Actions and Processes.
<br>
In order to start a term collection, we first must select the type of term we want to collect: action or process.
For that, we may use the combo box at the toolbar in section Collect.
<br>
<br>
<img border = "0" src="../images/optionsCollect.jpg" align="center">
<br>
<br>
After selecting the type of term, the second combo box will be updated to contain the names of the terms
that can be collected that are of the selected type. The simple selection of their names will trigger the
term's collection.
<br>
<br>
<img border = "0" src="../images/collectTerm.jpg" align="center">
<br>
<br>
In this case, only the development window is updated. It will indicated that a collection has taken place and, of course,
the collected term will also be shown.
<br>
<br>
<img border = "0" src="../images/collectedTermo.jpg" align="center">
<br>
<br>
Another way to make the term collection is using the pop-up menu in the development window. The "Collect Code" option of this
pop-up menu give two options (one for each term type): Action and Process. From these option, we can
select the desired term for collection.
<br>
<br>
<img border = "0" src="../images/collectTerm2.jpg" align="center">
<br>
<br>
</td>
</tr>
</table>
</body>
</html>