Specify which axioms are used in the following code block. Label each portion of the axiom that are present, show the parts that can be implied by the code present given the final post condition. This problem requires you to find a precondition for the code block. This problem requires you proving the total correctness of the loop. ...
length = arr. length;
sum = 0;
missing = 0;
for(int i = 0; i < length; i++){
if ( A[i] != null ){
sum = sum + arr[i] ;
} else {

missing++ ; }
}
length = length - missing;
average = sum / length; {
average = AVG(arr) for all nonempty elements of arr}