next up previous
Next: How to print RSL Up: A User Guide to Previous: How to create RSL

How to type check RSL specifications using rsltc

To syntax and type check a specification X, stored in a file X.rsl, open the file in emacs and choose RSL $\rightarrow$ Type check. 1

If there are errors, rsltc outputs messages in the form

X.rsl:m:n: text
which indicates that there is an error described by text in the file X.rsl at line m and column n.

As an example, consider the following erroneous specification:

 
  scheme COUNTER =
    class
      variable counter : Nat := 0
      value increase : Unit -> write counter Nat
      axiom increase() is counter := counter + true ; counter
    end
Type checking gives the following output:
  Checking COUNTER ... 
  COUNTER.rsl:5:46: Argument types Nat and Bool
  incompatible with `+' type Int >< Int -> Int or
  Real >< Real -> Real or
  Int -> Int or
  Real -> Real
  Finished COUNTER
  rsltc completed: 1 error(s) 0 warning(s)
After changing the specification to the correct version (section 3), type checking gives the following output:
    Checking COUNTER ... 
    Finished COUNTER
    rsltc completed: 0 error(s) 0 warning(s)



Anne Haxthausen 2003-03-13