What's new?

[Helene.Kirchner@loria.fr]

Dear all,

Here are some news from the Tools group:

Two new notes T-8 and T-9 have been installed:

Some Remarks on the Annotation %cons
Dieter Hutter
  http://www.brics.dk/Projects/CoFI/Notes/T-8/
  ftp://ftp.brics.dk/Projects/CoFI/Notes/T-8/

Executing CASL Equational Specifications with the ELAN Rewrite Engine
Hélène Kirchner and Christophe Ringeissen
  http://www.brics.dk/Projects/CoFI/Notes/T-9/
  ftp://ftp.brics.dk/Projects/CoFI/Notes/T-9/

-----------------------------------------------------------------
Web pages for Tools are available at
 
   http://www.loria.fr/~hkirchne/CoFI/Tools/

-----------------------------------------------------------------

Donald Baillie's CASLtoPVS tool is now available. 
from the page
	http://www.loria.fr/~hkirchne/CoFI/Tools/PROJECTS/provers.html
or directly at
	http://www.dcs.ed.ac.uk/~dts/cofi/CASLtoPVS

Here is below the characteristics of this new tool:

CASLtoPVS by Donald Baillie, Univ. of Edinburgh (address
correspondence to Don Sannella, dts@dcs.ed.ac.uk)

WHAT IS ITS PURPOSE?
Converting CASL basic specifications to the PVS specification
language, for use with the PVS prover.

WHICH SUBLANGUAGE OF CASL IS ADDRESSED?
Basic CASL with total functions only (except that partial selectors
are allowed and are converted into total functions into a subsort),
minus sort generation constraints and the membership predicate.

DOES THE TOOL CONFORM TO THE CASL SYNTAX?
Yes

DOES THE TOOL CONFORM TO THE INTERCHANGE FORMAT?
Yes

WHICH ARE THE RELEVANT ANNOTATIONS? 
None.  If %implies had the status of an approved annotation, this
would have been used and it should be easy to alter the program to
accept this.  Currently, it regards any axiom of the form
	forall f:THEOREM . phi
as indicating that phi is to be proved in the current specification.

HOW TO USE IT?  HOW TO INSTALL IT?
See the web page.  Basically, it converts a file name.aterm into a
file name.pvs with additional files corresponding to any datatypes
in the specification.