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

Re: Existence TCCs




Robert,

An existence TCC typically shows up when you are trying to
declare a constant of an uninterpreted type (TYPE).

T: TYPE

x: T

The decalaration of x in the above PVS fragment generates an
existence TCC.

You can make the existence go away by indicating to PVS that the
uninterpreted type being used is nonempty.  This can be done by using
TYPE+ instead of TYPE.  For example, the following PVS code will
not generate an existence TCC

T: TYPE+

x: T

Now, the explanation as to why PVS says "May need to add an assuming
clause to prove this" is as follows.  Typically the the uninterpreted
type (T in the above example) appears as a parameter to the PVS theory
in which x is being declared.  So, the PVS message reminds the user
that you may need to make certain assumption about T (in this case
that it is nonempty) to discharge the TCC.  Constraints about theory
parameters are given in a section called ASSUMING .... END ASSUMING at
the beginning of the theory declaration.  This is described in the
PVS Language Reference Manual.

I hope this helps.

- Srivas