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

Re: Don't understand this TCC

I have answered my own question (I'm pretty sure) concerning the TCC I'd
asked about, Tuesday March 28, 2000.  I think it's a useful enough point
to deserve putting the answer on the list.  If I've got it wrong I hope
someone will correct me when they have chance.  For the original question
read my original posting, quoted below.

Here's the short answer: to instantiate the extend operation as I've
attempted it, the function type [BD -> real] must be a subtype of [BD_HDS
-> real].  But this requires that the domain types be coextensive, and we
can't prove this; all we know is that BD is a subtype of BD_HDS.

Here's a longer answer:
The extend operation needs to be instantiated on four parameters,
extend[T1, T2, T3, x], where T1 T2 and T3 must be types and x an instance
of T3.  Plus, the type you pass in for T2 needs to be a subtype of the one
passed in for T1.

In my theory (reproduced in the quotation below), I have two types BD and
BD_HDS, the first declared to be a subtype of the second.  I then attempt
to instantiate the extend operation with the following two types passed in
for T1 and T2:

for T1:    [setof[BD_HDS],[BD_HDS -> real]]

for T2:    [finite_set[BD],[BD -> real]]

So the second type (call it "T2")  had better be a subtype of the first
("T1").  In the PVS type system, one tuple type is a subtype of another if
they have the same number, n, of component types, and for each k from 1 up
to n, the kth component type of the first is a subtype of the kth
component type of the second. This means that in the case at hand, in
order for T2 to be a subtype of T1, we must have it that

   1.  finite_set[BD] is a subtype of setof[BD_HDS]

   2.  [BD -> real] is a subtype of [BD_HDS -> real]

PVS is able to ascertain that the first claim holds, since BD was declared
a subtype of BD_HDS, but PVS cannot ascertain the second claim:  it
concerns two function types, and a function type is a subtype of another
only if the domain types are coextensive and the range type of the first
is a subtype of the second (see Rushby, Owre & Shankar "Subtypes for
Specifications: Predicate Subtyping in PVS", p.718).  So PVS generates a
TCC in connection with claim 2 requiring that we establish the
coextensiveness of BD and BD_HDS.  Which is unprovable since the only
information we have regarding these two types is that BD is a subtype of
BD_HDS.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
On Tue, 28 Mar 2000, Mark Aronszajn wrote:

> Can someone help?  I have a simple theory in which I try to introduce a
> generic, extended version of the real-valued sum operation for finite
> sets.  The theory takes two types as parameters, one declared to be "FROM"
> the other, the first intended to be the domain supertype for the extended
> version of sum, the other intended to be the original domain type. Here's
> the theory:
> 
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> Extended_Real_Summation[BD_HDS: TYPE, BD: TYPE FROM BD_HDS] : THEORY
> 
> BEGIN
> 
> IMPORTING finite_sets@finite_sets_sum_real[BD]
> 
> extended_real_sum: [[setof[BD_HDS],[BD_HDS -> real]] -> real] =
>   extend[[setof[BD_HDS],[BD_HDS -> real]],
>          [finite_set[BD],[BD -> real]],
>          real,
>          0](sum)
> 
> END Extended_Real_Summation
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> 
> When I typecheck this theory, I get the following TCC, which as I
> understand it, is not in general provable for all possible type actuals
> that could be passed in for the two type parameters:
> 
> extended_real_sum_TCC1: OBLIGATION
>   (FORALL (x: BD_HDS): BD_pred(x)) AND (FORALL (x: BD_HDS): BD_pred(x));
> 
> Isn't this asking me to show twice over that any instance the supertype
> is an instance of the subtype?  Why am I getting this TCC?
> 
> Thanks in advance for any help,
> 
> Mark Aronszajn
> 
> Reusable Software Research Group
> Dept. of Comp. Sci. & Elec. Eng.
> West Virginia University
> 
>