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

Re: Help with finding minimum in an array recursively



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))
>
>
>