Re: [PVS-Help] sequence filter

[David Coppit <pvs@coppit.org>]

On Wed, 28 Sep 2005, xu wrote:

> I want to write a function to implement the sequence filter, i.e.,
> remove some speical symbols of that sequence. for examples:

NOTE: This is not the complete answer. I'm learning too.

I guess I would have taken the sequence and set from the same type:

   filter: THEORY
   BEGIN

   S:TYPE+

   filter(seq:sequence[S],set:set[S]) : sequence[S] =
      IF member(first(seq), set) THEN
        filter(rest(seq),set)
      ELSE
        insert(first(seq), 0, filter(seq,set))
      ENDIF

   END filter

The type checker doesn't like how the return value of "rest" is a
sequence[S].sequence rather than a sequence[S]. I don't know enough about
parameterized theories to fix it. :(

David

_____________________________________________________________________
David Coppit                           david@coppit.org
The College of William and Mary        http://coppit.org/

"They have computers, and they may have other weapons of mass destruction."
Former Attorney General Janet Reno, speaking at LLNL of modern criminals