Use Hoare axiom for array-componenet assignment to determine the weakest pre-condition

Question

ASSERT( P ) /* determine what is P */

A[i] = A[m];

A[k] = 2;

ASSERT( A[i] == x + 5 )

Answer 1

I don't know about the weakest but I can tell you about candidate precondition,a[m] is assigned to a[i] so the range of m must concide with that of i,the postcondition is a[i]==x+5 so a[m]==x+5.

I have used the fact that array is a collection of tuples of index and value and thus the above result.