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

[PVS-Help] Local variables and the 'LET' strategy



Dear PVS users,

I am currently running PVS 3.1, and coding a number of new strategies. In most
of them I need to define local lisp variables, and therefore to use the (LET
...) strategy to declare and modify these variables.

However I cannot get PVS to do the modification part: it appears that setq
will not affect any variables declared using LET. Below is an example of this
behaviour: 

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

Rule? (let ((x 1)
            (dy (print (format nil "x is ~D, should be 1" x))))
        (then (let ((dy (setq x 2)))
                (lisp (print (format nil "x is ~D, should be 2" x))) )
              (lisp (print (format nil "x is ~D, should be 2" x)))) 
      )
"x is 1, should be 1" 
"x is 1, should be 2" 
"x is 1, should be 2"

ex0 :  

	|-------
	[1]   FORALL (x: real): x + 0 = 0 + x
				

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

Note that I cannot use a (let ((x 2)) ...) in place of the (setq x 2 ...) on
line 3 because this would only declare a new 'x' variable and not modify the
'x' declared on line 1. 

I read the Prover Guide but could not get any information on this topic. Is
there any other way to declare and modify local variables in strategies ?

Florent.

PGP signature