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

*To*: <brownmarco@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] How to avoid/discharge an Existence TCC for my subtype*From*: "Cesar A Munoz" <munoz@xxxxxxxxxx>*Date*: Thu, 17 Aug 2006 13:44:33 -0400 (EDT)*Cc*: pvs-help@xxxxxxxxxxx*Importance*: Normal*In-Reply-To*: <00c301c6c20c$8d0a0cc0$6801a8c0@rps.local>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <00c301c6c20c$8d0a0cc0$6801a8c0@rps.local>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Mark, One simple "solution" is to state MyConstant /= SecondConstant as an axiom and then use the axiom to prove the TCC1: test : THEORY BEGIN q: TYPE+ r: TYPE+ FROM q MyConstant, SecondConstant : r MyAxiom : AXIOM MyConstant /= SecondConstant s: TYPE+ = { ra: r | ra /= MyConstant } firstrs : s END test Obviously, using axioms is not a very good idea in general. An alternative solution may be to declare the types and the constants as parameters of the theory and to state MyConstant /= SecondConstant as an assumption in the assuming clause: test2[q:TYPE+,r:TYPE+ from q, MyConstant,SecondConstant:r] : THEORY BEGIN ASSUMING MyAssumption : ASSUMPTION MyConstant /= SecondConstant ENDASSUMING s: TYPE+ = { ra: r | ra /= MyConstant } firstrs : s END test2 In either case, you may introduce inconsitencies. Therefore, it is a good idea to provide a model of your theory. If you use axioms, you can provide a model by using theory interpretations: itest : THEORY BEGIN IMPORTING test {{ q := int, r_pred := LAMBDA(ra:int) : ra >= 0, MyConstant := 0, SecondConstant := 1 }} END itest If you use assumptions, you could define a theory that instantiate the types and constants with concrete elements: itest2 : THEORY BEGIN IMPORTING test2[int,nat,0,1] END itest2 Hope that this helps, Cesar Mark Brown said: > 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 -- Cesar A. Munoz H., Senior Staff Scientist National Institute of Aerospace 100 Exploration Way Hampton, VA 23666, USA Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988

- Prev by Date:
**[PVS-Help] How to avoid/discharge an Existence TCC for my subtype** - Next by Date:
**RE: [PVS-Help] How to avoid/discharge an Existence TCC for my subtype** - Prev by thread:
**[PVS-Help] How to avoid/discharge an Existence TCC for my subtype** - Next by thread:
**RE: [PVS-Help] How to avoid/discharge an Existence TCC for my subtype** - Index(es):