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

Re: [PVS] Survey on NASA PVS Library use



On Monday 13 September 2004 07:58, Adriaan de Groot wrote:

> One of the really nice things about manip is its means to specify formulas
> and subformulas. Having long constant strings based on a specific sequent
> form (say, in an (inst) command) makes PVS proofs somewhat brittle, and
> it'd be nice to have something more flexible, like
>
>         (inst -1 ('re 2 "Foo(.*)"))
>
> (which could mean "Match formula 2 against the RE Foo(.*) while keeping
> parens balanced and use that to (inst) in formula -1").

This kind of thing can already be done with Manip, although not quite as 
concisely as you wish.  There is RE-like pattern matching available plus 
other features for traversing expression trees to find subexpressions.  Your 
example could be done using this Manip construction:

    (invoke (inst -1 $1s) (! 2 (-> "Foo") 1))

Thanks for your general observations and descriptions of command usage.  While 
we recognize it takes some effort to learn how to use others' libraries and 
strategies, our experience has been that it pays off in the long run.  For 
our work in proving over the reals, in particular, we found that both 
libraries and strategies made a significant difference.

To make these artifacts more accessible, we're currently developing a database 
service to make libraries searchable and allow users to download what they 
need, when they need it.  We expect to make this new service publicly 
available by the end of the year.


-----

Ben Di Vito
1 South Wright Street, MS 130
NASA Langley Research Center
Hampton, VA 23681   USA

voice: +1-757-864-4883     fax: +1-757-864-4234
b.divito@nasa.gov
http://shemesh.larc.nasa.gov/people/bld