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

Re: VAR error


> % Subtype TCC generated (at line 151, column 31) for  updated_val
> % unfinished
> updating_state_TCC2: OBLIGATION
>   FORALL (rest: list[variable], var_1: variable, updated_val: value_list,
>           updated_var: list_of_vars):
>     updated_var = cons[variable](var_1, rest) AND NOT updated_val =
>       null[value] IMPLIES cons?[value](updated_val);
> Rule? (tcc) gives me this error msg
> ______________________ERROR MSG____________
> Found VAR when expecting
>   opsym, (, (#, [|, (:, identifier, IF, TRUE, FALSE, [||], !STRING!, 
> ____________________________________________
> Any idea why?

If you apply (TCC) to the above obligation, the prover first tries to
skolemize the formula, with (SKOSIMP*), I think.  In fact, this is the
command that produces the error message and it seems that it is not
able to correctly generate a name for the Skolem constants. I suspect
that it gets confused by the variable name "var_1" and mistakenly sees
a VAR keyword instead. 

This is a bug and you should send your error report to the PVS bug
mailing list pvs-bugs@csl.sri.com.

To finish your proofs you might either want to manually prove the TCCs
using something like 

	(skolem 1 ("rest!1" "var_1!1"  "updated_val!1" "updated_var!1"))

for the above TCC, or remove the underscore from variable names and
change them to "var1" etc.

Hope this helps,

	- Holger

Holger Pfeifer                          Tel.: +49 (0)731 / 50-24124
Universität Ulm                          Fax: +49 (0)731 / 50-24119
Abt. Künstliche Intelligenz        pfeifer@ki.informatik.uni-ulm.de
D-89069 Ulm        http://www.informatik.uni-ulm.de/ki/pfeifer.html