Demonstration Exercise 2

Problem 1: Verified Grades

  1. Write a function calculate_grade(num_n, num_r, num_m, num_e, num_core) that takes five arguments, the number of Ns, Rs, Ms, Es, and core LOs earned by a student in this course and returns a string corresponding to the major letter grade they earned, i.e., "A", "B", "C", "D", or "F". The calculation for overall grades in the course can be found in the course syllabus. Include your source code for this function in your demo write-up, ideally in a \begin{lstlisting} ... \end{lstlisting} source code block.

  2. State a property about calculate_grade that implies its correctness and formally prove that the property holds of your implementation. Your property must universally quantify over at least three of the parameters to calculate_grade. Otherwise, you are free to state any property of calculate_grade that could reasonably imply that your implementation is correct.

Problem 2: What's Wrong?

Consider the following erroneous implementation of a map_add(n, l) function which ought to add n to every element of a list of numbers l.

def cons(x, l):
    return [x, *l]

define map_add(n, l):
    match l:
        case []:
            return []
        case [head, *tail]
            return map_add(n, tail)

Part 1: Debug

In a sentence or two, describe what is wrong with this implementation.

Part 2: Debunk

Consider the following erroneous "proof" of the correctness of map_add.

Proof

Claim For any list of natural numbers l, map_add(0, l) ≡ l.

Proof. We proceed by induction on l.

  • Case: l is empty. Then the left-hand side evaluates as follows: map_add(0, l) --> [] ≡ l.

  • Case: l is non-empty. Let head and tail be the head and tail of l, respectively. Our induction hypothesis states that:

    IH: map_add(0, tail) ≡ l.

    The left-hand side evaluates as follows: map_add(0, l) -->* map_add(0, tail). By our induction hypothesis, map-add(0, tail) ≡ l, which completes proof.

Analyze the proof and in a sentence or two describe the error in the proof that allows the proof to go through.

Part 3: Deal With

Finally, replicate the proof, fixing the error identified in the previous step, and attempt to carry the proof to completion. Describe in a sentence or two where you get "stuck" in the proof and cannot proceed forward.

Problem 3: Zero Is The Hero

Part 1: Implement

Implement a recursive Python function dropzeroes(l) that takes a list l of numbers as input and returns l but with all 0s. For example dropzeroes([1, 3, 0, 1, 0, 2]) -->* [1, 3, 1, 2]. Make sure to test your code in Python and add your code to this write-up using a code block.

Part 2: Prove

Prove the following property of dropzeroes:

Claim (Idempotency of dropzeroes)

dropzeroes(dropzeroes(l)) ≡ dropzeroes(l)

(Hint: be precise with your program derivations and every step you make! In particular, make sure that every step is justified, and you consider all possibilities of evaluation.)