CS536 Assignment 3
Due: Feb 28th, 2025
Early Bird Due: Feb 26th, 2025
(Ethics: Any behavior on any homework or exam that could be considered copying or cheating will result in an immediate zero on the assignment
for all parties involved. See the IIT Code of Academic Honesty,)
1. Remember that Σ is the collection of all well-formed states, and Σ⊥ = Σ ∪ {⊥}. Decide true or false for each of
the following statements, justify your answers briefly.
a. If 𝜎(𝑝) =⊥, then ⊭ ¬𝑝.
b. Let 𝜏 ∈ Σ⊥, then 𝜏 ⊨ 𝑝 or 𝜏 ⊨ ¬𝑝.
c. Let Σ0 ⊆ Σ and Σ0 ⊨ 𝑝, also let 𝜏 ⊨ 𝑝; then Σ0 ∪ {𝜏} ⊨ 𝑝.
d. ∅ ⊨ 𝑝 and ∅ ⊨ ¬𝑝 (∅ represents an empty collection of states).
e. Let Σ0 ⊂ Σ, then Σ0 ⊨ 𝑥 > 1 or Σ0 ⊨ 𝑥 ≤ 1.
2. Calculate denotational semantics for the following nondeterministic programs.
a. Let 𝐼𝐹 ≡ 𝐢𝐟 𝑥 > 𝑦 → 𝑥 ≔ 𝑥 − 1 ◻ 𝑥 > 𝑦 → 𝑦 ≔ 𝑦 + 1 ◻ 𝑥 + 𝑦 = 4 → 𝑥 ≔ 𝑦/𝑥 ◻ 𝑥 + 𝑦 = 4 → 𝑥 ≔
𝑥/𝑦 𝐟𝐢, and let 𝜎1 = {𝑥 = 3, 𝑦 = 1}. Calculate 𝑀(𝐼𝐹, 𝜎1) and show your work.
b. Let 𝐼𝐹 ≡ 𝐢𝐟 𝑥 > 𝑦 → 𝑥 ≔ 𝑥 − 1 ◻ 𝑥 > 𝑦 → 𝑦 ≔ 𝑦 + 1 ◻ 𝑥 + 𝑦 = 4 → 𝑥 ≔ 𝑦/𝑥 ◻ 𝑥 + 𝑦 = 4 → 𝑥 ≔
𝑥/𝑦 𝐟𝐢, and let 𝜎2
(𝑥) = 𝜎2
(𝑦) = 1. Calculate 𝑀(𝐼𝐹, 𝜎2) and show your work.
c. Let 𝐷𝑂 ≡ 𝐝𝐨 𝑥 > 𝑦 → 𝑥 ≔ 𝑥 − 1 ◻ 𝑥 > 𝑦 → 𝑦 ≔ 𝑦 + 1 ◻ 𝑥 + 𝑦 = 4 → 𝑥 ≔ 𝑦/𝑥 ◻ 𝑥 + 𝑦 = 4 → 𝑥 ≔
𝑥/𝑦 𝐨𝐝, and let 𝜎1 = {𝑥 = 3, 𝑦 = 1}. Calculate 𝑀(𝐷𝑂, 𝜎1) and show your work.
d. Let 𝐷𝑂 ≡ 𝐝𝐨 𝑥 > 𝑦 → 𝑥 ≔ 𝑥 − 1 ◻ 𝑥 > 𝑦 → 𝑦 ≔ 𝑦 + 1 ◻ 𝑥 + 𝑦 = 4 → 𝑥 ≔ 𝑦/𝑥 ◻ 𝑥 + 𝑦 = 4 → 𝑥 ≔
𝑥/𝑦 𝐨𝐝, and let 𝜎2
(𝑥) = 𝜎2
(𝑦) = 1. Calculate 𝑀(𝐷𝑂, 𝜎2) and show your work.
3. Let 𝑏 be an array of size 𝑛 ≥ 1, and ∀0 ≤ 𝑖 < 𝑛. 𝑏[𝑖] = 0 ∨ 𝑏[𝑖] = 1. Decide which number (0 𝑜𝑟 1) is the
majority in 𝑏 without counting their quantities.
Write a program named 𝑀𝐴𝐽𝑂𝑅𝐼𝑇𝑌 in our language that can solve the above problem and bind the majority
among 0 and 1 to variable 𝑚𝑎𝑗𝑜𝑟. You can assume that 𝑏 is written in the memory state; and to simplify the
question, we artificially define 𝑏[𝑛] = 100, so you don’t need to worry about a possible runtime error when the
array index reaches 𝑛. Your program doesn’t have to be deterministic. Be careful of the grammar in our
programming language.
Here are some hints:
1) We can use the following linear-search-like algorithm: scan the array 𝑏 to pair up each 0 with a 1. Once we
have some 1′𝑠 left over, then 1 is the majority; once we have some 0′𝑠 left over, then 0 is the majority; if
we can pair up all numbers, then either of them can be the majority.
2) A student named Jason wrote a partial solution that could be useful to solve the above problem:
𝐽 ≡ 𝐝𝐨 𝑏[𝑘0
] = 1 → 𝑘0 ≔ 𝑘0 +1 ◻ 𝑏[𝑘1
] = 0 → 𝑘1 ≔ 𝑘1 + 1 𝐨𝐝
Consider 𝑘0 and 𝑘1 as pointers for number 0 and 1 respectively. What program 𝐽 does is to find the next
𝑘0 and 𝑘1
such that 𝑏[𝑘0
] = 0 and 𝑏[𝑘1
] = 1. You can use 𝐽 inside of your program.
4. Decide true or false for each of the following statements, justify your answers briefly.
a. If 𝑀(𝑆, 𝜎) contains exactly one state, then 𝑆 is a deterministic statement.
b. If 𝜎 ⊭ {𝑝} 𝑆 {𝑞}, then 𝜎 ⊨ 𝑝.
c. If 𝜎 ⊨𝑡𝑜𝑡 {𝑝} 𝑆 {𝑞}, then 𝜎 ⊭ 𝑝.
d. If 𝜎 ⊨ {𝑝} 𝑆 {𝑞}, then 𝑀(𝑆, 𝜎) ⊨ 𝑞.
e. If 𝜎 ⊭ {𝑝} 𝑆 {𝑞}, then 𝜎 ⊭𝑡𝑜𝑡 {𝑝} 𝑆 {𝑞}.
5. Answer the following questions about possible values of variable 𝑥 in a state. Justify your answer briefly.
a. Let ⊥𝑒∉ 𝑀(𝑆, 𝜎), where 𝑆 ≡ 𝑥 ∶= 𝑠𝑞𝑟𝑡(𝑥) / 𝑏[𝑥] and 𝜎(𝑏) = (3, 0,−2, 4). What are the possible values
of 𝜎(𝑥)?
b. Let 𝜎 ⊨ {𝑥 ≠ 0} 𝐰𝐡𝐢𝐥𝐞 𝑥 ≠ 0 𝐝𝐨 𝑥 ≔ 𝑥 −2 𝐨𝐝 {𝑥 < 0}, what are the possible values of 𝜎(𝑥)?
c. Let 𝜎 ⊨𝑡𝑜𝑡 {𝑥 ≠ 0} 𝐰𝐡𝐢𝐥𝐞 𝑥 ≠ 0 𝐝𝐨 𝑥 ≔ 𝑥 − 2 𝐨𝐝 {𝑥 < 0}, what are the possible values of 𝜎(𝑥)?
6. Let predicate function 𝑃(𝑘, 𝑠) ≡ 𝑠
2 ≤ 𝑘 ≤ (𝑠 + 1)
2
. For each of the following triples, decide whether it is valid
under total correctness, justify your answer briefly.
a. {𝑃(𝑘, 𝑠 +1)} 𝑠 ≔ 𝑠 + 1 {𝑃(𝑘, 𝑠)}
b. {𝑃(𝑘, 𝑠)} 𝑠 ≔ 𝑠 +1 {𝑃(𝑘, 𝑠 + 1)}
c. {𝑃(𝑘, 𝑠) ∧ 𝑠 < 0} 𝑠 ≔ 𝑠 + 1; 𝑘 ≔ 𝑘 + 1 {𝑃(𝑘, 𝑠)}
d. {𝑃(𝑘, 𝑠) ∧ 𝑠 = 𝑥} 𝑠 ≔ 𝑠 + 1 {𝑃(𝑘, 𝑥)}
e. {𝑃(𝑘 +1, 𝑠 + 1)} 𝑠 ≔ 𝑠 + 1; 𝑘 ≔ 𝑘 + 1 {𝑃(𝑘, 𝑠)}
7. Let 𝜎 ⊨ {𝑝1
} 𝑆 {𝑞1
} and 𝜎 ⊨ {𝑝2
} 𝑆 {𝑞2
}. Decide whether 𝜎 necessarily satisfies the following triples under
partial correctness, justify your answer briefly.
a. {𝑝1 ∧ 𝑝2
} 𝑆 {𝑞1 ∧ 𝑞2
}
b. {𝑝1 ∨ 𝑝2
} 𝑆 {𝑞1 ∨ 𝑞2
}
c. {𝑝1 ∨ 𝑝2
} 𝑆 {𝑞1 ∧ 𝑞2
}
8. Let ⊨𝑡𝑜𝑡 {𝑝1
} 𝑆 {𝑞1
} and ⊨𝑡𝑜𝑡 {𝑝2
} 𝑆 {𝑞2
}. Decide whether the following triples are valid under total
correctness, justify your answer briefly.
a. {𝑝1 ∧ 𝑝2
} 𝑆 {𝑞1 ∧ 𝑞2
}
b. {𝑝1 ∧ 𝑝2
} 𝑆 {𝑞1 ∨ 𝑞2
}
c. {𝑝2
} 𝑆 {𝑞1 → 𝑞2
}
Hints for questions 7 and 8:
1) Remember that 𝜎 ⊨ 𝑝 ∧ 𝑞 means “𝜎 ⊨ 𝑝 and 𝜎 ⊨ 𝑞”; 𝜎 ⊨ 𝑝 ∨ 𝑞 means “𝜎 ⊨ 𝑝 or 𝜎 ⊨ 𝑞”.
2) To prove 𝜎 ⊨ {𝑝} 𝑆 {𝑞}, you can prove that “if 𝜎 ⊨ 𝑝,then 𝑀(𝑆, 𝜎)−⊥ ⊨ 𝑞”.
3) To prove ⊨𝑡𝑜𝑡 {𝑝} 𝑆 {𝑞}, you can prove that “for any state 𝜎, if 𝜎 ⊨ 𝑝,then 𝑀(𝑆, 𝜎) ⊨ 𝑞”.
請加QQ：99515681 郵箱：99515681@qq.com WX：codinghelp
