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

Re: Help with finding minimum in an array recursively




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