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

[PVS-Help] How to avoid/discharge an Existence TCC for my subtype



Hello,

I am having trouble discharging or avoiding this existence TCC:

% Existence TCC generated (at line 199, column 2) for firstrs: s
  % unfinished
Firstrs_TCC1: OBLIGATION EXISTS (x: s): TRUE;

The TCC is generated when I declare my first constant of type s:

[199]  firstrs: s

I have declared s to be a subtype of a subtype as follows:

q: TYPE+
r: TYPE+ FROM q
MyConstant, SecondConstant: r
s: TYPE = { ra: r | ra /= MyConstant }

Alternatively, I get a slightly different Existence TCC that I don't know
how to discharge if I declare s as a "TYPE+" as in:

s: TYPE+ = { ra: r | ra /= MyConstant }

Either way, I'd like to create the TYPE s which contains everything in TYPE
r, except for one member.  Thanks in advance,

Mark