1. Provide a speci cation for the following program using predicate logic.
The program sets x to 1 when its input n is a left-truncatable prime, and sets x to 0 otherwise.
A left-truncatable prime is a prime number such that as you remove the left-most digits one
at a time the resulting number is still a prime number, e.g., 9137 is a left-truncatable prime
since each of the following are prime: 9137, 137, 37 and 7.
(3 marks)
2. The following program sets i to an index of the maximum element in array a.
fa:len > 0g
i = 0;
j = 1;
while (j 6= a:len)f
if (a[j] > a[i])fi = j;g
j = j + 1;
g
f8j : Z 0 j ^j < a:len)a[j] a[i]g
(a) Provide a loop invariant suitable for proving that the program is correct. Explain in
words why it is a loop invariant and why it is su cient to prove correctness.
(2 marks)
(b) Provide a proof of partial correctness of the program 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.
(4 marks)
(c) Validate your proof using KeY-Hoare (predicate logic parts of the proof may be per-
formed automatically). Save the .proof le for submission.
(1 mark)
3. The following program nds the index i of array a corresponding to the end of the longest
segment of consecutively increasing values starting from position 0.
i = 1; while (i 6= a:len^a[i 1] a[i])fi = i + 1;g
(a) Provide a formal speci cation for the program.
(3 marks)
(b) Provide a loop invariant suitable for proving that the program is correct. Explain in
words why it is a loop invariant and why it is su cient to prove correctness.
(3 marks)
(c) Provide a loop variant suitable for proving that the program terminates. Explain in
words why it is a loop variant and why it is su cient to prove termination.
(2 marks)
(d) Use Key-Hoare to prove that the program is totally correct (predicate logic parts of
the proof may be performed automatically). Save the .proof le for submission.
(2 marks)
4. This question is to be completed by CSSE7100 students only.
A repeat command has the form
repeat fSg until B
It executes S rst, then evaluates B. If B is true it terminates, otherwise it repeats the
repeat command from the beginning.
(a) Show how the repeat command can be represented in our simple while language.
(1 marks)
(b) Based on your answer to part (a), devise a Hoare Logic rule for the repeat command.
(3 marks)
Marking
The assignment is worth 20% of your nal grade. Each question is worth the marks indicated
adding to a total of 20 marks (for CSSE3100 students) and 24 marks (for CSSE7100 students).
A mark of zero will be given for work with little or no academic merit.
Submission
This assignment is due on Friday 23 March, 5pm. The following should be submitted by
Blackboard by the due date and time.
A le assignment1.pdf containing your answers to Q1, Q2(a) and (b), and Q3(a), (b) and
(c), and, for CSSE7100 students only, Q4(a) and (b).
A le maxElement.proof containing your proof for Q2(c).
A le longestInc.proof containing your proof for Q3(d).
Late submission: Please see Section 5.3 of the Course Pro le regarding extensions to assignment
due dates.
School Policy on Student Misconduct
This assignment is to be completed individually. You are required to read and understand the
School Statement on Misconduct, available on the Schools website at:
http://www.itee.uq.edu.au/itee-student-misconduct-including-plagiarism
Predicate logic rules
P;Q ‘RandLeft
P ^Q ‘R
‘P;QorRight
‘P _Q
Q ‘RimpRight
‘Q )R
‘P;QnotLeft
:P ‘Q
P ‘Q P ‘RandRight
P ‘Q ^R
P ‘R Q ‘RorLeft
P _Q ‘R
‘P;R Q ‘RimpLeft
P )Q ‘R
P ‘QnotRight
‘:P;Q
‘P[x=c]allRight
‘8x : A P
P[x=c]‘QexLeft
9x : A P ‘Q
8x : A P;P[x=t]‘QallLeft
8x : A P ‘Q
‘9x : A P;P[x=t]exRight
‘9x : A P
close P ‘P
closeFalse false‘P
closeTrue P ‘true
where c is an arbitrary constant, and t is a value or constant.
Hoare logic rules
fPg[x := e]SfQgassignment
fPg[ ]x = e; SfQg
fPg[U]SfQgskip
fPg[U]skip; SfQg
fP ^U(b)g[U]S1; SfQg fP ^U(:b)g[U]S2; SfQgconditional
fPg[U]if (b)fS1gelsefS2gSfQg
‘P )U(I) fI ^bg[ ]S1fIg fI ^:b)g[ ]SfQgloop
fPg[U]while(b)fS1gSfQg
‘P )U(I ^v 0) fI ^b^v = v0g[ ]S1fI ^v 0^v < v0g fI ^:b)g[ ]SfQgloop
T fPg[U]while(b)fS1gSfQg
‘P )U(Q)exit
fPg[U]fQg