Given two (possibly empty) arrays of integers a and b, with lengths a.len and b.len respectively,...1 answer below »

CSSE3100/7100 1. Provide a specification for the following program using predicate logic. Given two (possibly empty) arrays of integers a and b, with lengths a.len and b.len respectively, such that • array b does not contain duplicate elements, • array a may or may not contain duplicate elements, however it can only contain integers that are in array b the program does not modify b, but it sorts the elements of array a such that they appear in the order given by array b. For example, given that array a is initially [5, -1, 5, 0, -1, 5, 8, 5] and b is initially [0, 5, -1, 9, 8], the final value of array a should be [0, 5, 5, 5, 5, -1, -1, 8] and the final value of b should be [0, 5, -1, 9, 8] (the same as its initial value). You may use permutation(a, a0) to represent the predicate stating that array a is a permutation of array a0. You should assume that the arrays are indexed from 0. Your answer should be of the form requires P ensures Q where P is the precondition of the program and Q is the postcondition. Both P and Q must be expressed using predicate logic. (4 marks) 2. Consider the following Hoare triple in which variable a is an array of integers, len, x , i are integer-valued variables, and r is a Boolean-valued variable.

Document Preview:

Assignment 1 CSSE3100/7100
1. Provide a specication for the following program using predicate logic.
Given two (possibly empty) arrays of integers a and b, with lengths a:len and b:len respec-
tively, such that
array b does not contain duplicate elements,
array a may or may not contain duplicate elements, however it can only contain integers
that are in array b
the program does not modify b, but it sorts the elements of array a such that they appear in
the order given by array b. For example, given that array a is initially [5;1; 5; 0;1; 5; 8; 5]
and b is initially [0; 5;1; 9; 8], the nal value of array a should be [0; 5; 5; 5; 5;1;1; 8] and
the nal value of b should be [0; 5;1; 9; 8] (the same as its initial value).
You may use permutation(a; a0) to represent the predicate stating that array a is a permu-
tation of array a0. You should assume that the arrays are indexed from 0.
Your answer should be of the form
requires P
ensures Q
where P is the precondition of the program and Q is the postcondition. Both P and Q must
be expressed using predicate logic. (4 marks)
2. Consider the following Hoare triple in which variable a is an array of integers, len, x, i are
integer-valued variables, and r is a Boolean-valued variable.
f(0 len)g
i = 0;
r = false;
while (i < len)f
if (a[i] = x)f
r = true;
i = len;
gelsef
i = i + 1;
g
g
f(r = true), (9 k :Z (0 k^ k < len^ a[k] = x))g
We use Z to denote the set of integers, i.e., ..., -2, -1, 0, 1, 2, ... .
(a) Provide a loop invariant (using predicate logic) suitable for proving partial correctness
of the Hoare triple. Explain in words why it is a loop invariant and why it is sucient
to prove partial correctness.
(3 marks)
(b) Provide a proof ofpartial correctness of the Hoare triple using the Hoare Logic rules at
the end of this assignment, and arguing informally, i.e., in words, why the predicate logic
parts of the proof hold. The proof must be presented as a textual proof (as described in
lectures and...