1. Use the array-component assignment axiom (two times in case (b)) to find the weakest sufficient pre-condition P for the following code fragments: (a) (1 mark) ASSERT (P) /* determine what is P */ A[j] = A[i]; ASSERT A [K] >= A[j]) (b) (3 marks) ASSERT ( P ) /* determine what is P */ A[j] = 2; A[k] = x; ASSERT (A[i] == 5 ) Above x is an integer variable. A is an array of integers and we assume that all the subscripts are within the range of subscripts for A. In both cases, write the assertion P first using the notation from the array-component assignment axiom, and then rewrite P in a logically equivalent and simplified form that does not contain any notation (A | IE) (as in examples on pp. 85-86 and in examples covered in the videos).