代写CS536、代做C/C++，Java编程

日期：2025-02-19 10:05

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 𝑀(𝑆, 𝜎) ⊨ 𝑞”.