This is my own version of a small tutorial for Centaur, to be used as a complement to the Exp tutorial provided in the Centaur documentation. It provides a sample programming languages, with static semantics (in other words type discipline), operational semantics (concretely, this is an interpreter), and two kinds of program transformation: constant propagation and simplification.
An interesting complement to the centaur specification is that the language specifications have been translated into Coq specifications and the Coq system has been used to prove properties of the language, or more practically, properties of the tools built around this language.
The complete description of the little language is available at the following address:
ftp://ftp-sop.inria.fr/lemme/Yves.Bertot/little.tgz
To explain you how to make this work in Centaur, I will simply assume you have already installed Centaur in the directory that will be referred to by the variable $CentaurDir
As a first step, you have to download the file little.tgz on your machine. Let us suppose you place it in the directory /tmp.
As a second step you have to create a sub-directory contrib in your home directory and extract the downloaded archive there, for instance with the following commands:
cd $HOME/contrib gunzip -c < /tmp/little.tgz | tar xfz
Normally, that should be all you need to do. To test, just type the following command.
centaur -resfile $HOME/contrib/little/centaur.rdb
Using the Open in new option from the File menu, read in the file $HOME/contrib/little/examples/even.lil. You should obtain a window with the following shape:
You can select any sub-expression of the program by clicking on it with the left button of the mouse. Then, typing any character provokes this expression to be replaced by a plain text fragment, which you can edit character by charcter, also using navigation command inspired from Emacs: control-F (forward), control-B (backward), control-N (next line), control-P (previous line), control-D (delete current character), Delete, backspace (delete previous character), control-K (clear the rest of the line). When you are finished you can type Escape, this will provoke the parsing of the text fragment and the insertion of the corresponding program fragment in place of the selected expression. If you want to abandon text editing, you can also type control-G.
Using the option Beginner or Expert from the menu editing tool, you will be able to open a extra window, proposing editing operations that are valid for the selected expression in your program. (If no expression is selected, the window is empty, but it becomes active at the first selection).
Note that the option transformation/... is active only when you select an if or a while construct. Among the transformations proposed in this sub-menu, the options trivial_if and unfold_loop have been chosen because they don't change the semantics of the program (we even constructed a mechanically checked proof of this).
You can check whether the program is well-typed by selecting the option Typecheck from the little menu (also available with the right button of the mouse). This will only return a yes or no answer, visible in Centaur's main window.
You can execute the program to the end using the option Exec. At the end of the execution, this opens a window, named Final state, containing the value of all variables in the program.
You can perform transformations on the program. The first one, Propag will propagate constant values through the program. The action of this tranformation is not very visible on the example file even.lil. To test constant propagation, it may be better to work on the other example file provided: propagation_example.lil.
Constant propagation introduces many useless program fragments in the program. The second transformation, Simpl, simplifies these useless fragments away.
If you want to study the semantic specifications of all these analyses, executions, or transformations, all files are in the directory $HOME/contrib/little/semantics. Here is the correspondance:
| Typecheck | statics.ty |
| Exec | dynamics.ty, update.ty, eval.ty |
| Propag | propagation.ty, propag_eval.ty, glb.ty |
| Simpl | simpl.ty, rewrite.ty |
If you want to see the semantics specifications progress rule by rule on the program, you can choose the option Debug on from the little menu before choosing any of the semantic operations. This will open the Typol debugger on the program being studied. Have a look, it is very instructive!
Please note, that when the execution proceeds, the subject of the current rule is highlighted in the source window.