COMP1600 Assignment 2
The Austalian National University
School of Computing
Lecturer of the respective content
Copyright By PowCoder代写 加微信 powcoder
Foundations of Computation
Question 1 Structural Induction over Lists [2 + 3 + 3 + 11 + 6 Credits] Consider the functions filter, revAppend and length defined on lists of an arbitrary type a
filter :: (a -> Bool) -> [a] -> [a]
filter p [] = []
filter p (x:xs)
|px = x:(filter p xs) | otherwise = filter p xs
revAppend :: [a] -> [a] -> [a]
revAppend [] ys = ys
revAppend (x:xs) ys = revAppend xs (x:ys) — RA2
length :: [a] -> Int
length [] =0 — L1 length (x:xs) =1+lengthxs — L2
The goal of this exercise is to show that
length (filter p (revAppend xs ys)) = length (filter p xs) + length (filter p ys) holds for all lists xs and ys.
a) What precisely should we prove by induction? State a property P(xs), including possible quanti- fiers, so that proving this property by induction implies the (above) goal of this exercise.
b) For your chosen property P, state (including all possible quantifiers) and prove the base case goal.
c) State (including all possible quantifiers) the inductive hypothesis of the proof.
d) State (including all possible quantifiers) and prove the step case goal.
e) Explain using no more than 150 words how the base case and step case indeed prove the required property for all values of xs. You may reference induction principles, types and your property P among other things. (Note that this must be typed and submitted separately to turnitin)
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 [3 + 7 + 3 + 4 + 8 Credits] Consider the following definition of ternary trees of an arbitrary type a:
data TerTree a = Leaf a | Node a (TerTree a) (TerTree a) (TerTree a)
together with the functions height and size that compute the height, and the number of nodes in a
tree, respectively.
height :: TerTree a -> Int
height (Leaf x) = 0 — H1
height (Node a l m r) = 1 + maxThree (height l) (height r) (height m) — H2
size :: TerTree a -> Int
size (Leaf x) = 1 — S1
size (Node x l m r) = 1 + size l + size m + size r — S2
— F2 — F3
In order to do this, a new max function has been defined to calculate the max of three elements (maxThree), that is
maxThree :: (Ord a) => a -> a -> a -> a
maxThree x y z = max (max x y) z — M1
The type TerTree is an extension of the binary tree that we learnt in the lectures. Here each node has three children instead of two. So a non-leaf element of this type looks like Node a l m r, where a is the node value, l is the left child, m is the middle child, and r is the right child. While the leaves would take the form Leaf x.
Given that all elements of type TerTree a have to be constructed in one of those ways, this question is about identifying the correct induction principle for TerTrees and using it to show that the property
P(t) ≡ size t ≤ 3(height t)+1 − 1 2
holds for all elements t of type TerTree a.
a) Propose an induction principle that allows us to prove that a property P(t) holds for all elements
t of type TerTree a?
State the premises P1 and P2, including all necessary quantifiers, so that P1 P2 is a valid
induction principle for TerTrees.
b) Briefly justify your answer for (a), use no more than 300 words. Make sure to discuss at least the
following points:
Why the premises you defined are sufficient for the required principle. I.e., explain why proving
P1 and P2 is enough to conclude the property holds for all TerTrees.
What modifications you have made to the premises of the binary tree induction principle, and
why you decided that these were required.
You must submit this part as a typed file into turnitin.
To show that P(t) holds for all elements t of type TerTree a, we use structural induction (and the induction principle identified above in (a)).
c) State (including possible quantifiers) and prove the base case goal.
d) State (including possible quantifiers) the inductive hypotheses of the proof.
e) 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 maxThree function that computes the maximum of three numbers that you can justify with math (and no further justification is needed for that step).
Question 3 Hoare Logic (partial correctness) [5 + 15 + 5 Credits]
The program below, called foo, calculates x ∗ y and stores the value in r (‘%’ is the modulo operation, e.g. 345 % 10 = 5, and ‘/’ is integer division – division without reminder, e.g. 345 / 10 = 34):
while (m > 0)
if m%2=1 then
r := r + n;
m := m – 1
n := n * 2 ; m := m / 2;
(You may use the abbreviation ‘body’ to refer to the program inside the while loop, and ‘foo’ to refer to the entire program.)
The goal of this exercise is to show that foo conforms to its specification, i.e. to show that the Hoare triple
{(m = x) ∧ (n = y) ∧ (r = 0) ∧ (x ≥ 0)} foo {(r = x ∗ y)}
a) Find a suitable loop invariant I. Here suitable means
1. Theinvariantisestablished:(m=x)∧(n=y)∧(r=0)∧(x≥0)→I. 2. The postcondition is established: I ∧ ¬b → (r = x ∗ y).
3. The invariant is invariant: {I ∧ b}body{I}.
where b ≡ m > 0 is the loop condition. State the invariant, no proof required (yet).
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
{(m = x) ∧ (n = y) ∧ (r = 0) ∧ (x ≥ 0)} foo {(r = x ∗ y)}
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 (m > 0)
if m%2=1 then
r := r + n;
m := m – 1
n := n * 2 ; m := m / 2;
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 = k] body [I ∧ E < k]
where b ≡ m > 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 = k] body [I ∧ E < k]
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.
Release: Due: Mode: Submit:
individual submissions only
as single pdf file via Wattle (scans of legible handwritten solutions are perfectly acceptable) Sub questions 1 (e) and 2 (b) must be typed up and submitted into turnitin.
No marks will be provided for written solutions for these two questions.
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
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com