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

*To*: taylort@dg-rtp.dg.com*Subject*: Re: Why no TCC generated?*From*: John Rushby <RUSHBY@csl.sri.com>*Date*: Tue 30 Jun 98 17:31:07-PDT*Cc*: pvs-help@csl.sri.com*In-Reply-To*: <199806151950.PAA00822@happy.rtp.dg.com>*Mail-System-Version*: <SUN-MM(229)+TOPSLIB(128)@csl.sri.com>

Two weeks ago, Tad Taylor asked: > In the following theory, Set_MAC is a function from a Rule_Input to a > Rule_Output. A Rule is a subtype of this in which the function must > have various properties. I expected the first use of Set_MAC below to > generate a TCC where I'd be required to show that Set_MAC does indeed > satisfy the properties associated with a Rule. However, no TCC is > generated. > DG_Rules : THEORY > BEGIN > System_Rules : TYPE = setof[Rule] > DG_System_Rules : System_Rules = (LAMBDA (x : Rule) : x = Set_MAC) The reason no TCC is generated is that the equality is on the supertype--i.e., the type of Set_MAC. If you want to force the equality to be on the subtype you'd need to say x =[Rule] Set_MAC > The next line generates exactly the TCC I was expecting, > Set_MAC_Rule : Rule = Set_MAC You get a TCC here because you explicitly specify the type of Set_MAC_Rule to be Rule. Therefore Set_MAC is a valid value only if it satisfies the subtype predicate. John -------

**References**:**Why no TCC generated?***From:*taylort@dg-rtp.dg.com (Tad Taylor)

- Prev by Date:
**Re: COND and incomplete information** - Next by Date:
**Re: COND and incomplete information** - Prev by thread:
**Why no TCC generated?** - Next by thread:
**quantifier library** - Index(es):