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)
Copyright By PowCoder代写 加微信 powcoder
|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 x 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.
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com