Homework 10 Array Assignments

CS 536: Science of Programming Homework 10
Array Assignments
CS 536: Science of Programming, 

A. Why?
• Array assignments are more complicated than assignments to plain variables because they
require information known only at runtime (the value of the index).
B. Objectives
After this homework, you should know how to
• Perform textual substitution to replace an array element.
• Calculate the wp of an array element assignment.
C. Problems [60 points total]
Class 21: Array Assignments
1. [9 = 3*3 points] Syntactically calculate the following; you may simplify if you want.
a. wp(b[0] := 9, x > b[k])
b. wp(b[k] := b[m], b[m] = z)
c. wp(b[k] := 1, b[k] = b[m])
2. [6 points] Complete the full proof outline below for partial correctness by using wp to give
definitions for p₁ and then p₂. Logically simplify as you go. (Hint: Try using x ≠ y.)
{p₂} b[x] := b[m]; {p₁} b[y] := b[n] {b[x] < b[y] ∧ x ≠ y}
3. [35 points] The overall goal is to calculate wp(b[x] := x, b[x] = b[b[y]]). It's complicated, so
we'll do it in parts. The hardest part is fully calculating (b[b[y]])[x⧸b[x]]. Unoptimized, (b[b[y]])
[x⧸b[x]] ≡ if e₁ = x then x else b[e₁] fi, where e₁ ≡ (b[y])[x⧸b[x]].
a. [3 points] Expand e₁ ≡ (b[y])[x⧸b[x]] to get an if-fi expression.
b. [9 points] Let e₂ ≡ (e₁ = x). Expand e₂ and logically simplify. (The simplest answer is a
disjunction of two terms.)
 This is the last homework for the semester! 1
CS Dept., Illinois Institute of Technology – 1 – © James Sasaki, 2021
CS 536: Science of Programming Tue 2022-11-15, 19:28 Homework 10: Class 21
c. [6 points] Let e₃ ≡ b[e₁]. Expand e₃ and arithmetically simplify it by changing it from a b[…]
of an if-fi to an if-fi with b[…] inside.
d. [14 points] Let e₄ ≡ (x = if e₁ = x then x else b[e₁] fi). Substitute your e₂ for (e₁ = x) and your
e₃ for b[e₁], and simplify the result: Push the x = … part of the test into the arms of the if-fi
and continue from there. The simplest result is a disjunct of three terms, but getting there
is complicated. A hint: (if T then B else … fi 㱻 B) and (if F then … else B fi 㱻 B).
e. [3 points] Now calculate wp(b[x] := x, b[x] = b[b[y]]) ≡ (b[x])[x⧸b[x]]) = (b[b[y]])[x⧸b[x]].
(This should be easy.)
CS Dept., Illinois Institute of Technology – 2 – © James Sasaki, 2021