Why no TCC generated?

[taylort@dg-rtp.dg.com (Tad Taylor)]

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.  The next line generates exactly the TCC I was expecting,
but I don't want to say this for every rule in the system.

Can someone help me understand why the first use of Set_MAC doesn't
generate a TCC and while the second one does?  Thanks,

Tad

/* Tad Taylor                  |      919-248-6374           */
/* Data General Corporation    |      taylort@dg-rtp.dg.com  */
/* 62 T.W. Alexander Dr.       |                             */
/* RTP, NC 27709               |      FAX: 919-248-6108      */
                >> SDA - Standard Disclaimers Apply <<


DG_Rules : THEORY

BEGIN

IMPORTING Rules, test_rule

System_Rules : TYPE = setof[Rule]

DG_System_Rules : System_Rules = (LAMBDA (x : Rule) : x = Set_MAC)

Set_MAC_Rule : Rule = Set_MAC

END DG_Rules

---

• Prev by Date: Re: quantifier library
• Next by Date: PVS @ Linux other than RedHat
• Prev by thread: Re: PVS @ Linux other than RedHat
• Next by thread: Re: Why no TCC generated?
• Index(es):
  • Date
  • Thread