[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Generation of (E)Lisp code from PVS specification

The PVS Ground Evaluator generates Common Lisp code corresponding to a
PVS specification. The package PVSio, available from

 http://research.nianet.org/~munoz/PVSio

re-implements the interface to the Ground Evaluator and provides a
predefined library of imperative programming language features to PVS
(to be only executed by the ground evaluator).

For example, you can write:

% test.pvs 
% To typecheck this file use M-x load-prelude-library PVSio

test : THEORY 
BEGIN

  hello : void = println("Hello World")
 
  fibo(n:nat) : RECURSIVE nat =
    if    n = 0 then 0
    elsif n = 1 then 1
    else fibo(n-1)+fibo(n-2)
    endif
  MEASURE n
 
END test

You can "run" this "specification" (as a matter of fact any ground
functional specification) in the Emacs interface of PVS or directly in
the shell command line, e.g.,

$ pvsio test:hello
Hello World
==>
TRUE

$ pvsio 'test:fibo(4)'
==>
3

$ pvsio 'test:fibo(10)'
==>
55

Cesar

On Thu, 2005-06-02 at 05:41, Aditya Kanade wrote:
> Hi,
> 
> Is there any package for generating ELisp code corresponding to a
> PVS specification? Any suggestions for doing this kind of stuff are
> welcome. Does one has to walk over the parse tree generated by PVS?
> Any packages for doing this?
> 
> Regards,
> Aditya Kanade.
> Ph.D. student, CSE, IIT Bombay.
> http://www.cse.iitb.ac.in/~aditya
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way                 http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988