How to create RSL specifications in text files

RSL specifications are written in ordinary text files. Use emacs to edit a specification of an RSL module with name X in a file with name X.rsl. You must use ascii equivalents for the non-ascii RSL symbols. A table of ascii equivalents can be found on page 385 of the RSL book.

Here is an example of a specification to be stored in a file with the name COUNTER.rsl:

 
  scheme COUNTER =
    class
      variable counter : Nat := 0
      value increase : Unit -> write counter Nat
      axiom increase() is counter := counter + 1 ; counter
    end

If a module depends on other modules, their names (without ``.rsl'') should appear as a comma separated list at the start of the file. This list is the module's context. The tool calculates the transitive closure of contexts, so if A depends on B and B depends on C then you must include C as the context for B, and you may for the context of A use either B or B, C. The files A.rsl, B.rsl, and C.rsl must all be in the same directory. When a module is checked, the context modules are checked first, so you only need to run the tool on top level modules.