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 CASLtoPVS.java and his MSc report is in report.html. Questions should be addressed to Don Sannella (dts@dcs.ed.ac.uk) ================================================================ 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 http://www.wins.uva.nl/pub/programming-research/software/aterm/ (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 http://www.informatik.uni-bremen.de/~cofi/CASL/parser/parser.html 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 http://adam.wins.uva.nl/~markvdb/cofi/aterms-basic.html (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. USE --- 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. TO DO ----- In basic specs - membership predicate - sort generation constraints Generally - test for appropriate relationship between sorts (locally upward filtered or stricter) - structured constructs Donald Baillie, October 1999
Name Last modified Size Description
aterm-0.18/ 1999-12-23 09:31 - casl_parser/ 1999-10-26 16:05 - examples/ 1999-10-26 16:13 - README-DTS 1999-10-15 14:58 394 aterms-basic.html 1999-10-14 16:25 13K CASLtoPVS.class 2000-04-11 16:26 21K CASLtoPVS.java 1999-10-19 17:19 36K report.html 1999-10-21 13:03 64K