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

Re: [PVS-Help] sequence filter



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