The Austalian National University Semester 2, 2021
School of Computing Assignment 2
Victor Rivera and Dirk Pattinson
Foundations of Computation
Release: Friday, 03 September, 2021, 18:00 AEST
Due: Friday, 01 October, 2021, 23:55 AEST
Mode: individual submissions only
Submit: as single pdf file via Wattle (scans of legible handwritten solutions are perfectly acceptable), here.
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
https://wattlecourses.anu.edu.au/mod/assign/view.php?id=2380786
https://www.anu.edu.au/students/academic-skills/academic-integrity
https://www.legislation.gov.au/Details/F2015L02025
https://cs.anu.edu.au/courses/comp1600/policies/#academic-integrity
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] length :: [a] -> Int
tail [] = [] — T1 length [] = 0 — L1
tail (x:xs) = xs — T2 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 — LE1
leaves (LNode l r) = leaves l + leaves r — LE2
2
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
∀t.P (t) is a valid induction
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):
foo
while (i > 0)
if i%2=0 then
v := v*v;
i := i/2
else
j := j*v;
i := i-1
body
(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}
is valid.
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:
foo
while (i > 0)
if i%2=0 then
v := v*v;
i := i/2
else
j := j*v;
i := i-1
body
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. The variant is positive: 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. 4 1 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’. • Sequence: {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} 5 2 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’. • Sequence: [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. 6 Appendix — Hoare Logic Rules (partial correctness) Appendix — Hoare Logic Rules (total correctness)