The Austalian National University School of Computing
Victor Rivera and
Semester 2, 2021 Assignment 2
Release: Due: Mode: Submit:
Friday, 03 September, 2021, 18:00 AEST
Friday, 01 October, 2021, 23:55 AEST
individual submissions only
as single pdf file via Wattle (scans of legible handwritten solutions are perfectly acceptable), here.
Foundations of Computation
Pledge of Academic Integrity and Originality statement1
I am committed to being a person of integrity. I pledge, as a member of the Australian National University community, to abide by and uphold the standards of academic integrity outlined in the ANU statement on honesty and plagiarism. I understand that it is wrong to ever misrepresent another person’s work as my own.
I am aware of the relevant legislation, and understand the consequences of me breaching those rules. I have read the COMP1600/COMP6260 academic integrity and pledge to abide by it.
I declare that everything I have submitted in this assignment was entirely my own work.
Name: UID:
Signature:
1Submissions without your name, UID and signature will not be marked. 1
Question 1 Structural induction over lists [3 + 6 + 3 + 13 Credits] Consider the functions tail and length defined on lists of an arbitrary type a
tail :: [a] -> [a]
tail [] = []
tail (x:xs) = xs
— T1 — T2
length :: [a] -> Int
length [] = 0 — L1
length (x:xs) = 1 + length xs — L2
together with the following function overlay that takes two lists (of an arbitrary type a) and puts the first list on top of the second:
overlay :: [a] -> [a] -> [a]
overlay [] ys = ys — O1
overlay (x:xs) ys = x:(overlay xs (tail ys)) — O2
The goal of this exercise is to show that
length (overlay xs ys) = max (length xs) (length ys) holds for all lists xs and ys.
a) What precisely should we prove by induction? State a property P(xs), including possible quan- tifiers, so that proving this property by induction implies the (above) goal of this exercise.
b) For your chosen property P, state (including possible quantifiers) and prove the base case goal.
c) State (including possible quantifiers) the inductive hypothesis of the proof.
d) State (including possible quantifiers) and prove the step case goal.
In all proofs indicate the justification (e.g. the line of a definition used) for each step. You may assume basic properties of the max function that computes the maximum of two numbers that you can justify with math.
Question 2 Structural Induction on Trees [5 + 6 + 3 + 11 Credits]] Consider the following definition of binary trees of an arbitrary type a which only have elements at
the leaves:
data LTree a = Leaf a | LNode (LTree a) (LTree a)
together with the functions height and leaves that compute the height, and the number of leaf nodes
in a tree, respectively.
height :: LTree a -> Int
height (Leaf x) = 0 — H1
height (LNode l r) = 1 + max (height l) (height r) — H2
leaves :: LTree a -> Int
leaves (Leaf x) = 1
leaves (LNode l r) = leaves l + leaves r
— LE1 — LE2
The type LTree is different from the type Tree discussed in the lectures. An LTree is either a Leaf (that carries an element of type a), or an LNode, consisting of a right and left subtree (but no element of type a). Given that all elements of type LTree a have to be constructed in this way, this question is about identifying, the correct induction principle for LTrees, and using it to show that the property
P(t)≡leaves t≤2height t
holds for all elements t of type LTree a.
a) What induction principle allows us to prove that a property P(t) holds for all elements t of type LTree a?
State the premisses P1 and P2, including possible quantifiers, so that P1 P2 is a valid induction ∀t.P (t)
principle for LTrees, and briefly justify your answer.
To show that P(t) holds for all elements t of type LTree a, we use structural induction (and the
induction principle identified above in (a)).
b) State (including possible quantifiers) and prove the base case goal.
c) State (including possible quantifiers) the inductive hypotheses of the proof.
d) State (including possible quantifiers) and prove the step case goal.
In all proofs indicate the justification (e.g. the line of a definition used) for each step. You may assume basic properties of the max function that computes the maximum of two numbers that you can justify with math.
Question 3 Hoare Logic (partial correctness) [5 + 15 + 5 Credits] The program below, called foo, calculates xn and stores the value in j (‘%’ is the modulo operation,
e.g. 345 % 10 = 5, and ‘/’ is integer division – division without reminder, e.g. 345 / 10 = 34):
while (i > 0)
if i%2=0 then
v:=v*v;
i := i/2 body
j:=j*v;
(You may use the abbreviation ‘body’ to refer to the program inside the while loop.)
The goal of this exercise is to show that foo conforms to its specification, i.e. to show that the Hoare triple
{n ≥ 0 ∧ j = 1 ∧ i = n ∧ v = x} foo {j = xn}
a) Starting with the equation xn = j ∗ vi, find a suitable loop invariant I. Here suitable means
1. The invariant is established: n ≥ 0 ∧ j = 1 ∧ i = n ∧ v = x → I. 2. The postcondition is established: I ∧ ¬b → j = xn.
3. The invariant is invariant: {I ∧ b}body{I}.
where b ≡ i > 0 is the loop condition. State the invariant, no proof required (yet). 3
b) Using invariant I found in (a), or otherwise, prove that {I ∧ b} body {I}
is valid in the Hoare-calculus for partial correctness. Justify each step in your proof.
c) Continue the proof in (b) to prove that
{n ≥ 0 ∧ j = 1 ∧ i = n ∧ v = x} foo {j = xn}
is valid in the Hoare-calculus for partial correctness. Justify each step in your proof.
Question 4 Hoare Logic (total correctness) [5 + 15 + 5 Credits] Consider the (same) program foo:
while (i > 0)
if i%2=0 then
v:=v*v;
i := i/2 body
j:=j*v;
We now only want to prove that this program terminates, i.e. without making guarantees about the variables after execution. In other words, we want to show that the triple
[True] foo [True]
is provable in the Hoare-calculus for total correctness.
a) Identify and state a suitable invariant I and variant E for the loop. Here suitable means
1. The invariant is established: True → I
2. The postcondition is established: I ∧ ¬b → True
3. Thevariantispositive:I∧b→E≥0
4. The variant decreases, and the invariant is invariant: [I ∧ b ∧ E = n] body [I ∧ E < n].
where b ≡ i > 0 is the loop condition. State the variant and invariant, no proof is required (yet).
b) Using your variant E and invariant I in (a) give a proof of the Hoare triple
[I ∧ b ∧ E = n] body [I ∧ E < n]
in the Hoare-calculus for total correctness. Justify each step of your proof.
c) Continue the proof in (b) to prove that
[True] foo [True]
in the Hoare-calculus for total correctness. Justify each step of your proof.
Appendix — Hoare Logic Rules (partial correctness)
Assignment:
{Q(e)} x := e {Q(x)}
Precondition Strengthening:
Ps →Pw {Pw}S{Q} {Ps} S {Q}
You can always replace predicates by equivalent predicates,
i.e. if Ps ↔ Pw; just label your proof step with ‘precondition equivalence’.
Postcondition Weakening:
{P}S{Qs} Qs →Qw {P} S {Qw}
You can always replace predicates by equivalent predicates,
i.e. if Qs ↔ Qw; just label your proof step with ‘postcondition equivalence’.
{P} S1 {Q} {Q} S2 {R} {P}S1;S2 {R}
Conditional:
{P ∧b} S1 {Q} {P ∧¬b} S2 {Q} {P} if b then S1 else S2 {Q}
While Loop:
{I ∧ b} S {I}
{I} while b do S {I ∧ ¬b}
Appendix — Hoare Logic Rules (total correctness)
Assignment:
[Q(e)] x := e [Q(x)]
Precondition Strengthening:
Ps →Pw [Pw]S[Q]
[Ps] S [Q]
You can always replace predicates by equivalent predicates,
i.e. if Ps ↔ Pw; just label your proof step with ‘precondition equivalence’. Postcondition Weakening:
[P]S[Qs] Qs →Qw [P] S [Qw]
You can always replace predicates by equivalent predicates,
i.e. if Qs ↔ Qw; just label your proof step with ‘postcondition equivalence’.
[P] S1 [Q] [Q] S2 [R]
[P]S1;S2 [R] Conditional:
[P ∧b] S1 [Q] [P ∧¬b] S2 [Q] [P] if b then S1 else S2 [Q]
While Loop (Total Correctness):
I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]
[I] while b do S [I ∧ ¬b]
where n is an auxiliary variable not appearing anywhere else.