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

*To*: <qgxu@mail.shu.edu.cn>*Subject*: Re: [PVS-Help] sequence filter*From*: "Cesar A Munoz" <munoz@nianet.org>*Date*: Thu, 29 Sep 2005 23:07:06 -0400 (EDT)*Cc*: munoz@nianet.org, pvs-help@csl.sri.com*Importance*: Normal*In-Reply-To*: <007e01c5c3c8$eb618700$7601a8c0@x31088>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <007e01c5c3c8$eb618700$7601a8c0@x31088>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

There are at least two aspects to this question: 1. About the declarations: There are several ways to write this kind of polymorphims in PVS and S : TYPE+ T: TYPE FROM S f(a) : sequence[T] = ... may be one of them, but not the usual one. In this case, the predefined predicate T_pred could be used to check if a particular element of the sequence S is in T, e.g., if s is of type S, T_pred(s) holds if s is also an element of the type T. The simplest way to write this polynomorphism is using a parametric theory and a higher-order function: filter[S:TYPE+] : THEORY BEGIN test? : VAR PRED[S] % The filtering test is a predicate over S a : VAR sequence[S] f (a,test?) : sequence[(test?)] = ... % The output is a sequent of elements that satify test? END filter 2. About sequences: Note that sequences in PVS are always infinite (and they *do not* contain finite sequences as subtype). In particular, there is no "empty" sequence, nor is defined the "length" of a sequence. Also note that recursion is problematic with infinite sequences, for this reason David's solution does not work. If you want finite sequences, the type you need is finseq. In this case filter can be defined quite easily using a recursion. filter[S:TYPE+] : THEORY BEGIN a : VAR finseq[S] test? : VAR PRED[S] filter(a,test?): RECURSIVE finseq[(test?)] = if a`length = 0 then a elsif test?(a`seq(0)) then (a^(0,0)) o filter(a^(1,a`length),test?) else filter(a^(1,a`length),test?) endif MEASURE a`length END filter Now, if you really want infinite sequences then you probably have noticed that a filter is not defined for an arbitrary test. For example, if S is 0 1 2 3 ... and the test is x < 10, then the output is a finite sequence of 10 elements which is not a "sequence". In this case you need a stronger precondition on the sequence and the test to guarantee that the output of the filter is a "sequence". The definition is quite more involved and left to the reader :-) Cesar xu said: > > pvs-help: > > I am very new to PVS. > I want to write a function to implement the sequence filter, i.e., > remove some speical symbols of that sequence. for examples: > > S:TYPE+ > > a: VAR sequence[S] > > T: TYPE FROM S > > f(a) : sequence[T] % i want the f(a) only include the symbols type > of T. > > how to write this function f? > > can you help me! > thanks in advance! > > > Q.g., XU > > > qgxu@mail.shu.edu.cn > 2005-9-27 -- Cesar A. Munoz H., Senior Staff Scientist National Institute of Aerospace 100 Exploration Way Hampton, VA 23666, USA Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988 -- Cesar A. Munoz H., Senior Staff Scientist National Institute of Aerospace 100 Exploration Way Hampton, VA 23666, USA Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988

**References**:**[PVS-Help] sequence filter***From:*"xu" <qgxu@mail.shu.edu.cn>

- Prev by Date:
**Re: [PVS-Help] sequence filter** - Next by Date:
**[PVS-Help] (no subject)** - Prev by thread:
**Re: [PVS-Help] sequence filter** - Next by thread:
**[PVS-Help] Confused about proving extensionality of overriddenfunctions** - Index(es):