CRefine

Development

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.

##### Applying Refinement Laws

In order to apply a refinement law, we must select a specific term. This selection is realised on the lines of the development window; hold the CTRL key and click on the first and last line of the term in order to select multiple lines.
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.
Go to "Apply Law" on the menu and select the desired law in the pop-up menu if you wish to apply the law.
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.
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.
After selecting the law, the text field will store the law name. If the law is applicable to the selected term, the button will be enabled. Hence, the law may be applied.
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 Law details option.
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.
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 Virtual Keyboard.
After giving the arguments, the law application takes place. In this moment, the Development and Code window are updated. The Proof Obligation 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 Law Details.

##### Collecting Code

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.
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.
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.
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.
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.