Extracting positive elements of an array

June 22, 2010 – 6 years, 9 months ago, by Vladimir Klebanov

Short Description

Verify a program producing a new array containing only
positive elements of some given other array.

Code

int[] m(int t[]) {
    int i, count = 0;
    for (i=0; i < t.length; i++)
        if (t[i] > 0) count++;
    int[] u = new int[count];
    count = 0;
    for (i=0; i < t.length; i++)
        if (t[i] > 0) u[count++] = t[i];
    return u;
}

Specification

informal, see above.

Long Description

Prove that in

u[count++] = ...
the index is not out-of-bounds of array
u

Submitted by

Claude Marché


Solution:

The separation analysis in the Why platform is able to automatically
separate

t
and
u
.

Reference: http://www.lri.fr/~marche/hubert07hav.pdf

Submitted by

Claude Marché