Navigation
1 Changes to RSL
1.1 With expressions
1.2 Comments
1.3 Prefix + and -
1.4 == symbol
1.5 Finite maps
1.6 Extra meanings for ∈, ∉, and
hd
1.7 Test cases
1.8 Features of RSL not supported
2 Putting RSL into files
2.1 Mathematical characters
2.2 Contexts
3 Tool components available
4 Type checker
5 Pretty printer
6 Confidence condition generation
7 Showing module dependencies
8 Drawing a module dependency graph
8.1 Long file names in Windows
9 SML translator
9.1 Introduction
9.2 Activating the SML translator
9.3 Declarations
9.4 Class expressions
9.5 Object expressions
9.6 Type expressions
9.7 Value expressions
10 C++ translator
10.1 Introduction
10.2 Activating the C++ translator
10.3 Declarations
10.4 Variable declarations
10.5 Class expressions
10.6 Object expressions
10.7 Type expressions
10.8 Value expressions
10.9 Bindings
10.10 Names
10.11 Identifiers and operators
10.12 Universal types
10.13 Input/output handling
10.14 An example
11 PVS translator
11.1 Introduction
11.2 Activating the PVS translator
11.3 Declarations
11.4 Class expressions
11.5 Object expressions
11.6 Type expressions
11.7 Value expressions
11.8 Bindings and typings
11.9 Names
11.10 Identifiers
12 UML to RSL translator
12.1 Introduction
12.2 General Description of UML2RSL
12.3 Distribution Files
12.4 Installation
12.5 Using UML2RSL
12.6 UML Class Diagram Supported Features
13 SAL Translator
13.1 Introduction
13.2 Translatable RSL constructs
13.3 Writing transition systems and LTL assertions
13.4 Confidence condition verification
13.5 Using the tool
14 Use with emacs
14.1 Emacs on Windows
15 Mutation testing
16 Test coverage support
17 LaTeX support
18 Installation
18.1 Unix and Linux
18.2 Windows
19 Making it yourself
20 Help and bug-reporting
Acknowledgements
References
Navigation
Chris George, April 17, 2008