maxsummarizationpost-conditions

The max searching algorithm

Dear Experts and enthusiasts,

I would like to solve the following problem: I have an array of natural numbers. I would like to find their maximum.

But I have to show my solution with structogram, like that http://www.testech-elect.com/pls/images/casetool2.jpg

and I have to do this with midifieing the summation algorithm, this means that I have to midifie the structogram and postcondition of http://cfhay.inf.elte.hu/~hurrycane/programozas/programming_theorems.pdf

The main horizontal lines have to be kept, but you can modifie everything else. Can you tell me the modified postcondition without recursion? It would be enough. I can make the structogram if I get it. Thank you in advance.

Solution

  • Consider the C++ code for your algorithm:

    max = a[0]; ind = 0;
for (int i = 1; i < n; i++)
{
    if (a[i] > max)
    {
        max = a[i];
        ind = i;
    }
}

    For the above algorithm, we would have:

    1. StateSpace = (a : N*, n : N, ind : N, max : N)
    2. Pre-condition = (a = a' /\ n = length(a))
    3. Post-condition = (Pre-condition /\ (max, ind) = MAX(i = 0, n) a[ i ])