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

Help with finding minimum in an array recursively




Hello,

I tried to find out the minimum in an array recursively but am facing
problems. Could someone help me out with this.

I am sending the pvs code and the tcc generated.

Thank you in advance,
Nikhil

-------------PVS CODE------------------------------------

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  % math resolution to find min in array of real numbers
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  lower, upper, current: VAR posnat
  Sequence: TYPE = ARRAY[nat -> real]
  TypeSeq: VAR Sequence
 lowerupperAX: AXIOM lower <= upper

 RecSeqMin(TypeSeq,lower,current,upper):RECURSIVE nat = if (current <
upper) then RecSeqMin(TypeSeq,if TypeSeq(current+1) < TypeSeq(lower)THEN current+1
ELSE
lower ENDIF,current+1,upper) ELSE lower ENDIF

MEASURE lower

%basic function to be called
 SeqMin(TypeSeq, lower, upper): real = TypeSeq(RecSeqMin(TypeSeq,lower,lower,upper))



-----------------------TCC generated----------------------------
% Termination TCC generated (at line 52, column 82) for
    % RecSeqMin(TypeSeq,
    %           IF TypeSeq(current + 1) < TypeSeq(lower)
    %             THEN current + 1
    %           ELSE lower
    %           ENDIF,
    %           current + 1, upper)
  % unfinished
RecSeqMin_TCC1: OBLIGATION
  FORALL (TypeSeq: Sequence, current: posnat, lower: posnat,
          upper: posnat):
    (current < upper) IMPLIES
     IF TypeSeq(current + 1) < TypeSeq(lower)
       THEN current + 1
     ELSE lower
     ENDIF
      < lower;