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

[PVS-Help] Free Variables Not Allowed



Hey all,
       Was wondering if i could ask a little help, quite new to pvs and am just
trying to write a little recursive function that asks "chess pieces" if they
can move to a specific position on a board, i am having an issue with an error
about unallowed free variables. Any help much appreciated:

-------CODE-------

ClientCode : THEORY
BEGIN

IMPORTING ChessPiece
IMPORTING sets

Pieces: TYPE = set[ChessPiece]

s: VAR Pieces
r,c: VAR posint
x: var ChessPiece

recursiveCanAttack(s, r, c): RECURSIVE bool  = (

	IF(nonempty?(s)) THEN
		IF (member(x, s)) THEN
			IF (canAttack(x) OR canAttack(remove(x, s), r, c)) THEN
				TRUE
			ELSE
				FALSE
			ENDIF
		ELSE
			FALSE
		ENDIF
	ELSE
		FALSE
	ENDIF
	
) MEASURE Card(s)

END ClientCode

-------CODE-------

-------ERROR -----

Expecting an expression
No resolution for x
                  
 There is a variable declaration with this name,
 but free variables are not allowed here.

-------ERROR -----

regards
Roja

-----------------------------------------------------------------
University of St Andrews Webmail: http://webmail.st-andrews.ac.uk