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

*To*: pvs-help@csl.sri.com*Subject*: Re: Don't understand this TCC*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Thu, 30 Mar 2000 10:09:35 -0500 (EST)*Delivery-Date*: Thu Mar 30 07:12:02 2000*In-Reply-To*: <Pine.GSO.4.21.0003282301260.12495-100000@escher>

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

**References**:**Don't understand this TCC***From:*Mark Aronszajn <aronsz@csee.wvu.edu>

- Prev by Date:
**Don't understand this TCC** - Next by Date:
**reasoning with typepreds** - Prev by thread:
**Don't understand this TCC** - Next by thread:
**How to prove this** - Index(es):