Description

Homework 2: State and IMP
Prof. Stefan Muller
Updated Sept. 18
This assignment contains 7 written task(s) for a total of 65 points.
Logistics
Please read and follow these instructions carefully.
Submit your written answers in a single PDF or Word document. Typed answers are preferred (You can use any program as long as you can export a .pdf, .doc or .docx; LaTeX is especially good for typesetting logic and math, and well worth the time to learn it), but legible handwritten and scanned answers are acceptable as well.
Your Blackboard submission should contain only the file with your written answers. Do not compress or put any files in folders.
This homework is to be completed individually. Read the policy on the website and be sure you understand it.
1 State
Task 1.1 (Written, 8 points).
Let σ = {x = 5,y = 2,z = 1,a = [8;2;5]}.
For questions where the answer is a state, please give it as a set of variable-value pairs (e.g., {x = 5,y = 2,z = 1,a = [8;2;5]}, not as a state update).
a) What is σ[x 7→ 3][x 7→ 5]?
b) What is σ[w 7→ 4](w)?
c) What is σ[y 7→ 7][w 7→ 8]?
d) What is |σ(a)|?
Task 1.2 (Written, 12 points).
For each of the following, say whether the satisfaction holds or not. If not, why? a)
b)
c)
d)
Task 1.3 (Written, 8 points).
For each of the situations below, fill in the blanks to describe when the situation holds. Fill in with “some”, “all” or “no”.
a) ∃x ∈ Z.∀y ∈ Z.p if for states σ, it is true that σ[x →7 α1][y →7 α2] p for α1 ∈ Z and α2 ∈ Z.
b) ¬(∀x ∈ Z.∃y ∈ Z.q) if for states σ, it is true that σ[x →7 α1][y 7 → α2] q for α1 ∈ Z and α2 ∈ Z (Updated 9/18: Typo fix).
2 IMP Syntax and Semantics
Task 2.1 (Written, 15 points).
Evaluate each of the following expressions with the state
σ = {x = 5,y = 2,z = 1,w = T,v = F,a = [8;2;5]}
a) σ(x ∗ y)
b) σ(if x > y then x − z else y − z)
c) σ(a[z] + x)
d) σ(w ∨ v)
e) σ(a[size(a) − z])
Task 2.2 (Written, 8 points).
Write a program (statement) in the syntax of IMP that “truncates” an array a to length x, setting any elements after that to 0.
You can assume that both a and x are in the state at the beginning of the program.
If S is your program, and hS,σi →∗ hskip,σ0i, then for all 0 ≤ i < x, we should have σ0(a[i]) = σ(a[i]) and for all x ≤ i < |σ(a)|, we should have σ0(a[i]) = 0.
As an example, if σ = {a = [1;2;3;4;5],x = 3}, then σ0(a) = [1;2;3;0;0].
If x ≥ |σ(a)| (i.e., x is bigger than the length of a), then the array is not changed.
If x ≤ 0, then σ0(a) should have all 0s.
It’s OK if your program changes the value of x.
Your program should never access an out-of-bounds array element for any proper state (a state that contains values for both x and a).
Task 2.3 (Written, 14 points).
Consider the program S = while x > y do x := y od, in the state σ = {x = 3,y = 2}.
a) Evaluate the program using the small-step operational semantics we saw in class, i.e., give a series of configurations such that hS,σi → hS0,σ0i →∗ hskip,σ00i.
b) What is M(S,σ)? Explain how you know (potentially by showing your calculation, but other explanations are also acceptable).
3 One more wrap-up question
Task 3.1 (Written, 0 points).
How long (approximately) did you spend on this homework, in total hours of actual working time? Your honest feedback will help us with future homeworks.