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

Re: Help with finding minimum in an array recursively

  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.


  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
                 IF TypeSeq(current+1) < TypeSeq(lower)
                  THEN current+1
                  ELSE lower
                 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))