This is CASLtoPVS, a program to convert basic specifications in CASL
to PVS, written by Donald Baillie as his MSc project in Computer
Science at the University of Edinburgh in 1998/99.

This is the file README.  The program is in and his MSc
report is in report.html.

Questions should be addressed to Don Sannella (


CAStoPVS is written in Java and should work under both Solaris and
Linux.  It imports the Java ATerm library, which is written in Java1.2
and can be found at

(there is a copy in the directory aterm-0.18).

The program works on the output of the HOL-CASL parser and checker,
which is available from

in versions for Sparc-solaris or Linux.  There is a copy of the
Linux v0.21 parser in the directory casl_parser.  If example.casl
contains a CASL specification,

  casl_parser/casl -s example

produces a file example.aterm containing an aterm representing the
parse tree, and a file example.env containing information about the
environment created by the specification.

The structure of the program is therefore based on the mapping of the
syntax of basic CASL specifications onto ATerms used by the HOL-CASL
parser, which can be found at

(copy in aterms-basic.html).

NB treatment of recursively defined predicates in the program is
different from my report (section 4.1.4).   They are treated
identically to recursive functions and do not make use of the
'INDUCTIVE' construct in PVS as suggested by the report.


To use CASLtoPVS set up java1.2.  Then type 'java CASLtoPVS path/name'
where 'path' is a directory path relative to the current directory and
'name' corresponds to a file called 'name.aterm', as output by the
parser.  Of course, you need to compile CASLtoPVS first, unless you
are using Linux for which an object file is supplied.

The program then creates a directory 'name' containing a file
'name.pvs' along with further files corresponding to any free
datatypes defined in the specification.  All these files should then
be usable with PVS.  After 'cd name', the command to get started is

  pvs name.pvs

See the examples directory for some simple examples.


In basic specs 
 - membership predicate
 - sort generation constraints

 - test for appropriate relationship between sorts (locally upward
   filtered or stricter)
 - structured constructs

Donald Baillie, October 1999
      Name                    Last modified      Size  Description
aterms-basic.html 1999-10-14 16:25 13K README-DTS 1999-10-15 14:58 394 1999-10-19 17:19 36K report.html 1999-10-21 13:03 64K casl_parser/ 1999-10-26 16:05 - examples/ 1999-10-26 16:13 - aterm-0.18/ 1999-12-23 09:31 - CASLtoPVS.class 2000-04-11 16:26 21K