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

*To*: pvs-help@csl.sri.com*Subject*: Why no TCC generated?*From*: taylort@dg-rtp.dg.com (Tad Taylor)*Date*: Mon, 15 Jun 1998 15:50:11 -0400

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):