To syntax and type check a specification X, stored in a file
X.rsl, open the file in emacs and choose RSL Type check.
1
If there are errors, rsltc outputs messages in the form
X.rsl:m:n: textwhich 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 endType 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)