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

Re: Why no TCC generated?

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
> 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.