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

No Subject



Aaron,

This problem has been reported as bug # 466.  It will be fixed in the
next patch release.

Proofchain analysis checks whether there are any circular references in a
given proof.  This is mostly a sanity check, as circular references
shouldn't be possible in the first place.  There are two exceptions to
this: recursive functions and inductive definitions.  Unfortunately, when
inductive definitions were added we failed to update the proofchain
analysis code.

Regards,
Sam Owre

> Date: Tue, 1 Aug 2000 16:40:25 +0200 (MET DST)
> From: Aaron Ballard <aaron.ballard@mchp.siemens.de>
> To: pvs-help@csl.sri.com
> Cc: aaron.ballard@mchp.siemens.de
> 
> 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