johalj11__Jasraj+Johal__2023-10-20_18:41:35.241112_EDT_MARKING-2023-11-05_20:38:30.012529_EST.calcnb — Score: 6/39

Midterm 1 Notebook 2B: Command Correctness — (≈ 46%)

The setup here is the same as in A1.3, that is, sequences and command correctness material. The head and tail material from A1.3 is included here, too:

Declaration: head : Seq A → A
Declaration: tail : Seq A → Seq A
Axiom “Definition of `head`”: head (x ◃ xs) = x
Axiom “Definition of `tail`”: tail (x ◃ xs) = xs
Theorem “Non-empty-sequence extensionality”:
    xs ≠ 𝜖   ⇒   xs = (head xs ◃ tail xs)

Four hint items per hint are allowed here.

We provide an additional function for “flattening” a sequence of sequences, and give it the same name concat as in Haskell. For example:

    concat ((2 ◃ 8 ◃ 𝜖) ◃ (5 ◃ 𝜖) ◃ (3 ◃ 7 ◃ 𝜖) ◃ 𝜖) = 2 ◃ 8 ◃ 5 ◃ 3 ◃ 7 ◃ 𝜖

This is defined using the catenation operator _⌢_ from H13 (type \catenate for that symbol). This operator has its associativity activated here.

1:  Declaration: concat : Seq (Seq A) → Seq A
2:  Axiom “Definition of `concat` for 𝜖”:  concat 𝜖 = 𝜖
3:  Axiom “Definition of `concat` for ◃”:  concat (xs ◃ xss) = xs ⌢ concat xss

For warm-up, prove the following:

1:  Theorem (C2): ∃ ks : Seq ℤ • ∃ ns : Seq ℤ • concat (ks ◃ ns ◃ 𝜖) = 𝜖
2:  Proof:
3:      (∃ ks : Seq ℤ • ∃ ns : Seq ℤ • concat (ks ◃ ns ◃ 𝜖) = 𝜖)
4:    ⇐⟨ “∃-Introduction” ⟩
5:      (∃ ns : Seq ℤ • concat (ks ◃ ns ◃ 𝜖) = 𝜖)[ks ≔ 𝜖]
6:    ≡⟨ “Substitution into ∃”⟩
7:      

A linear-time imperative implementation of concat for sequences that are implemented as singly-linked lists can be achieved via a loop with the following program:

    xss := xss₀ ⍮
    ys := 𝜖 ⍮
    while xss ≠ 𝜖 do
        ys := ys ⌢ head xss ⍮
        xss := tail xss
    od

The following theorems constitute part of proving this correct with respect to the following postcondition:

    ys = concat xss₀

For the proofs, proceeding “backwards” as in Ex3.7 is recommended; this means that you will have a sequence of steps using calculation operators of the following shapes:

• ⁅ _ := _ ⁆⇐
• ⇐
• ≡

Each of these needs to be justified by a hint enclosed in ⟨ … ⟩ as usual, for example:

      a = 42
    ⁅ a := 7 · 8 ⁆⇐   ⟨ “Assignment” with substitution ⟩
      7 · 8 = 42
    ⇐                 ⟨ “ex falso quodlibet” ⟩
      false

You should not need additional lemmas.

 1:  Theorem “Initialisation for `Concat`”:
 2:        true
 3:      ⇒⁅ xss := xss₀ ⍮ ys := 𝜖 ⁆
 4:        ys ⌢ concat xss = concat xss₀
 5:  Proof:
 6:      ys ⌢ concat xss = concat xss₀
 7:    ⁅ xss := xss₀ ⁆⇐ ⟨ “Assignment” with Substitution ⟩
 8:      ys ⌢ concat xss₀ = concat xss₀
 9:    ⁅ ys := 𝜖 ⁆⇐ ⟨ “Assignment” with Substitution ⟩
10:      𝜖 ⌢ concat xss₀ = concat xss₀
11:    =⟨ “Left-identity of ⌢” ⟩
12:      concat xss₀ = concat xss₀
13:    =⟨ “Reflexivity of =” ⟩
14:      true
15:    ⇐⟨ “Reflexivity of ⇒”⟩
16:      true

1:  Theorem “Postcondition for `Maximum`”:
2:        ¬ (xss ≠ 𝜖) ∧ ys ⌢ concat xss = concat xss₀
3:    ⇒  ys = concat xss₀
4:  Proof:
5:    

1:  Theorem “Invariant for `Maximum`”:
2:        xss ≠ 𝜖 ∧ ys ⌢ concat xss = concat xss₀
3:      ⇒⁅ ys := ys ⌢ head xss ⍮ xss := tail xss ⁆
4:        ys ⌢ concat xss = concat xss₀
5:  Proof:
6:      

Concluding Declarations

Your answers above are completely your own work? (“No answer” is wrong.)

•  Yes
•  No

The text box below is the report box: If you want to leave us any message(s) that will be read when we mark the midterm, please select “Yes” here and write your message(s) in the text box below, by hitting ENTER with focus on that box.

•  Yes, I have entered messages below.
•  No, there are no relevant messages below.

(The text boxes allow Markdown; hit Ctrl-ENTER to see the layout result.)

Report box: Add your messages here (after hitting ENTER on this box).

.