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

*To*: pvs-help@csl.sri.com*Subject*: Don't understand this TCC*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Tue, 28 Mar 2000 23:14:30 -0500 (EST)*Delivery-Date*: Tue Mar 28 20:16:47 2000

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

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