CS 536: Science of Programming - HW 2: Expressions, States Satisfaction, State Updates
Types, Expressions, States, Quantified Predicates
CS 536: Science of Programming, Spring 2023 Due Thu Feb 2, 11:59 pm
2023-02-01: p.2
A. Formatting and Submitting Your Work
- Remember to use a word processor to write out your answers. Quantified variables range over Z unless otherwise specified.
- To speed up grading, be sure to include your group number and a list of the group members' userids and A# numbers. Use *.pdfs, not *.doc files.
- In all the problems below, assume that variables written with different names are ≢ unless explicitly said otherwise. (So with x and y, assume x≢y, but if we define “v≡x or y”, we don't necessarily know if v≡x or v≢x.)
B. Problems [60 points total]
Class 3: Types, Expressions, and Arrays
1. (4 points) Let b be a two-dimensional array. Is the expression b[ 0 ] + b[ 2 ] [ 3 ] legal or illegal according to the syntax we're using. If illegal, why? If legal, what is the type of the resulting expression?
2. (4 points) Is {u=(4), w=u[1], r=one, s=four, t=r+s} a well-formed state? If not, why?
3. (6=2*3 points) Let σ={x=2, b=β} where β=(7,12,3). Complete these equivalent definitions of σ:
a. σ={x=2, b={(0,7), ...
b. σ={x=2,b[0]=7,...
4. (8=2*4 points) Take the expression c*b[b[k]]. For each state below, is it well-formed; if it is, is it also proper for the expression? If it is, does the expression terminate correctly (and with what result)? If not, why?
a. {k=0, b=(3,6,1,4),c=2}
b. {k=0, b=3}
Class 4: State Updates, Satisfaction of Quantified Predicates
5. (8=2*4 points) Let σ={x=2, y=4}.
a. Whatisσ[x↦1];whatisσ∪{(x,1)};aretheyequal? b. Whatisσ[v↦2];whatisσ∪{(v,2)};aretheyequal?
6. (8=2*4 points) Let σ={x=2,y=4}. (Assume x≢y.)
- What is σ[x↦σ(y)][y↦σ(x)]? (Be careful)
- Let τ=σ[x↦3][y↦τ(x)*4]. What is τ? (Be careful)
7. (8 = 2 * 4 points) For each of the following, say whether the state satisfies the quantified predicate (and if not, briefly why). Give a witness value (for satisfied existentials) or a counterexample (for unsatisfied universals).
a. Does{x=0,b=(5,3,6)} ⊨(∀x.∀k.0<k<3∧x<b[k])?
b. Does{b=(2,5,4,8)}⊨(∃m.0≤m<4→b[m]<2)?
8. (4 points) Explain (in words): When does the following property hold?
⊭(∃x∈V.(∃y∈U.P(x,y))∧(∀z∈W.Q(x,z)))
9. (10 points) Write a definition for a predicate function Unique ( b , x , m ) that yields true when the m array elements starting with b [ x ] have unique values (i.e., m array locations, m different values). For example, Unique((1,2,3,2),1,2) is true but [2023-02-01] Unique((1,2,3,2),1,3) is false because it contains 2 twice. If m<0 or any of the indexes x, x + 1, etc. are illegal, return false. If you like, you can assume that ∧ and ∨ are short-circuiting, like&&and||inCandJava. Feelfreetodefinehelperpredicatesifyouwant.
