 | 2 Putting RSL into files |
| 
| Top |
| 
| 4 Type checker |
|
| 3 Tool components available |
3 Tool components available
There is a collection of related component tools, nearly all based on
the type checker rsltc. They are invoked from the command
line as shown below.
|
Command | Component |
|
rsltc <file> | Type check |
|
rsltc -pp <file> | Parsing (no type check) plus pretty printing
of current module |
|
rsltc -c <file> | Type check plus confidence condition generation
on current module |
|
rsltc -cc <file> | Type check plus confidence condition
generation on all modules |
|
rsltc -d <file> | Parsing (no type check) plus display of module
dependencies |
|
rsltc -g <file> | Generation of VCG file to show module dependencies |
|
rsltc -m <file> | Translation to SML |
|
rsltc -c++ <file> | Translation to C++ |
|
rsltc -cpp <file> | Translation to Microsoft's Visual C++ |
|
rsltc -pvs <file> | Translation to PVS |
|
UML2RSL <xml-file> | Translation to RSL from UML |
|
|
rsltc commands
These tool components are described in the following sections.
A more convenient interface to the rsltc tool components can be
obtained using emacs -- see section 14.
See section 12.5 for more information on invoking the UML
to RSL translator.
Chris George, April 17, 2008
| 3 Tool components available |
| 2 Putting RSL into files |
| |
| Top |
| |
| 4 Type checker |
|