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

Re: [PVS-Help] symbol manipulation

On Wednesday 05 May 2004 21:13, R. Colvin wrote:
> I have a defined strategy 'f' which takes as a formal parameter, 'name'
> (which is a predicate).  In addition to using 'name', I'd also like
> to use the symbol formed by prepending "inv_" to 'name'.
> That is, if I invoke the strategy f with actual parameter "foo", I
> also want to make use of the symbol "inv_foo".  
> I can do this by adding a parameter to f and invoking f(foo,
> inv_foo), but I'd prefer to just invoke f(foo), and internally to f
> construct the symbol inv_foo.  Can I do this inside a strategy
> definition?

You certainly can do it.  Here's an example:

(defstep two-names (name)
  (let ((inv-name (intern (format nil "inv_~A" name)))
        (msg (format nil "My names are ~A and ~A." name inv-name)))
    (skip-msg msg t))
  "" "")

The Common Lisp function "intern" maps a string to a symbol.


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