How can I prove the correctness of this multiplication algorithm?

Question

I want to know how I can prove that this algorithm is correct:

begin
array <- array with n integer unordered
max <- MININT
for i <-0 to n-1 do
    v <- 1
    for j <- i to n-1 do
        v <- v * array[j]
        if max < v then
            max   <- v
            first <- i
            last  <- j + 1
        endif
    endfor
endfor
Print max
end

PS: I am trying to find the max value of a subarray multiplication of my array. subarray multiplication mean the product of all the numbers in a sequence of consecutive entries of arbitrary with length great or equal 1

Example: array = {2,-1,0,2,1} The answer is 2 of subarray = {2,1}

Answer 1

Rewrite your algorithm to be a little less hard on the eyes:

MaxConsecutiveProduct(A) {
  Max = -infinity
  for (I in A.Range) {
    V = 1
    for (J in A.Range) {
      V *= A[J]
      if (Max < V) [Max, First, Last] = [V, I, J]
    }
  }
  return [Max, First, Last]
}

Write down what you are trying to prove. Let $R$ be the range of $A$:

$$\begin{align} \text{MaxConsecutiveProduct}(A)[0] &= \underset{C \in \text{AllConsecutiveSubArrays}(A)}{\text{Max}} \prod C \\ &= \underset{(I \times J) \in (R \times R)}{\text{Max}} \prod_{K=I}^J A[K] \end{align}$$

Notice that for this, First and Last are irrelevant. So we create an equivalent procedure that doesn't contain First and Last, as well as converting V to an array for the sake of proof:

MaxConsecutiveProduct(A) {
  Max = -infinity
  for (I in A.Range) {
    V[I][-1] = 1
    for (J in A.Range) {
      V[I][J] = V[I][J-1] * A[J]
      if (Max < V[I][J]) Max = V[I][J]
    }
  }
  return [Max]
}

The 'if' statement can converted to serial execution, then condenced:

MaxConsecutiveProduct(A) {
  for (I in A.Range) {
    V[I][-1] = 1
    for (J in A.Range) {
      V[I][J] = V[I][J-1] * A[J]
    }
  }

  Max = -infinity
  for (I in A.Range) {
    for (J in A.Range) {
      if (Max < V[I][J]) Max = V[I][J]
    }
  }

  return [Max]
}

This condencing can be proven with induction, but it is just an excercise in calculus. A logic like Hoare logic is what you would use.

MaxConsecutiveProduct(A) {
  V[I][J] = \prod_{K=1}^{J} A[K]
  Max = max(V)
  return [Max]
}

Now it is obvious that the procedure implements the desired function.