Re: Help with finding minimum in an array recursively

[Natarajan Shankar <shankar@csl.sri.com>]

Nikhil:
 I can't reproduce your problem.  Please send a dump file
(using M-x dump-pvs-files and the PVS version number so that we can
work with your exact setup.

-Shankar

> From:    Nikhil Varma <n_varma@ece.concordia.ca>
> Subject: Re: Help with finding minimum in an array recursively 
> Date:    Sun, 4 May 2003 04:54:10 -0400 (EDT)
> To:      <pvs-help@csl.sri.com>
> 
> A new problem has arisen when I do a M-x tcp if goes fine but when I do a
> M-x tcc of the following code I get the following error
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> Found ( when expecting
>   opsym, identifier, IF, TRUE, FALSE, [||], (||), or {||}
> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> I have also got the same problem in many other places. I would be very
> thankful if someone would help me with this
> 
> Nikhil
> 
> 
> On Wed, 30 Apr 2003, Natarajan Shankar wrote:
> 
> >
> > Nikhil:
> >   I've massaged your definition a bit
> > to add subtype information to the arguments.
> > This makes the TCCs (automatically) provable.
> >
> > The axiom
> >  lowerupperAX: AXIOM lower <= upper
> > is clearly false as is apparent by instantiating
> > lower with 2 and upper with 1.   It is risky to
> > add axioms about existing datatypes, and the right approach
> > here is to add subtype predicates to the corresponding
> > bound variables.
> >
> > Cheers,
> > Shankar
> >
> >   lower, upper, current: VAR posnat
> >   Sequence: TYPE = ARRAY[nat -> real]
> >   TypeSeq: VAR Sequence
> >
> >  RecSeqMin(TypeSeq,lower, (upper : upfrom(lower)),
> >            (current: subrange(lower, upper))) : RECURSIVE
> >        subrange(lower, upper)
> >    = IF (current < upper) then
> >       RecSeqMin(TypeSeq,
> >                  IF TypeSeq(current+1) < TypeSeq(lower)
> >                   THEN current+1
> >                   ELSE lower
> >                  ENDIF,
> >                  upper, current+1)
> >      ELSE lower ENDIF
> > MEASURE upper - current
> >
> > %basic function to be called
> >  SeqMin(TypeSeq, lower, (upper : upfrom(lower))): real
> >  = TypeSeq(RecSeqMin(TypeSeq,lower,upper,lower))
> >
> >
> >