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

No Subject



Hello,
PVS has generated for me the following two TCCS:


% Subtype TCC generated (at line 214, column 6) for  l
  % proved - incomplete
ns_TCC2: OBLIGATION
  FORALL (l: list[event]):
    NOT Nil(l) AND ns(cdr[event](l)) IMPLIES l /= null[event];

% Subtype TCC generated (at line 214, column 6) for  l
  % proved - complete
ns_TCC3: OBLIGATION
  FORALL (P: [list[event] -> boolean], l: list[event]):
    NOT Nil(l) AND P(cdr[event](l)) IMPLIES l /= null[event];

I think that if the second is complete, the first, which seems to be
an instantiation of the second, should be too.  If I use M-x-spc on
the first one, PVS says that the proof chain is complete, but
generates a warning that the TCC is circular on the definition of ns.
The same warning is generated for every later theorem that uses the
definition of ns.

Here is the definition of ns:


ns(l:list[event]):INDUCTIVE bool=
	Nil(l) OR
	(ns(cdr(l)) AND (
	Fake(l) OR
	NS1(l) OR
	NS2(l) OR
	NS3(l)
	))

If I comment out the portion for ns(cdr(l)), no TCCS are generated.
Can someone please explain why this inductive definition is circular?

Thanks,
Aaron Ballard