Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: THEend8_
SENG 2011 Assignment
Welcome to the first assignment. Some notes:
• The total number of marks of the exercises
will be scaled to 15 marks for the course assessment.
• In the Dafny exercises, – Please make sure your code verifies with
the CSE dafny verifier. – None of the exercises requires you to compile code,
or generate output. – In general, there is not a single correct spec of a program.
Specs may differ in efficiency, readability, conciseness and structure. All can affect the assessment. –
If performance is a factor, this will be stated. – Use the given predicate, method and file names exactly.
The auto-marker is case-sensitive. – Do not use the assume statement or function methods in this course.
ex1 4 marks The domain of the following predicates is the real numbers: P (x, y) : x > y Q(x, y) : x ≤ y R(x) : x + 42 = 99 S(x) :
x > 42 For each of the following statements, give the truth value, and justify in words the truth value. i ∀x∃yP (x, y) ii ∃y∀xQ(x, y)
iii ∀x∀y(P (x, y) ∨Q(x, y)) iv ∃xR(x) v ∀y(¬S(y)) vi (∃xS(x)) ∧ ¬(∀xR(x)) vii ∃y∀x(S(y) ∧Q(x, y)) viii ∀x∀y((R(x) ∧ S(y))⇒ Q(x, y))
Submit the file ex123.pdf, which should contain the solution to this exercise and ex2 and ex3. ex2 6 marks If P , Q,
R and S are logical propositions, prove ((P ⇒ (Q ∨R))⇒ ((¬Q ∨ S) ∧ ¬S))⇒ ¬Q using just the axioms below. a) P ∨ false ⇔ P b) P ∨
true ⇔ true c) P ∧ ¬P ⇔ false d) P ∧ false ⇔ false e) P ∨ ¬P ⇔ true f) P ∧Q ⇒ P g) P ∧Q ⇒ Q h)
P ∧Q ⇔ Q ∧ P i) ¬(P ∨Q) ⇔ ¬P ∧ ¬Q j) (P ∨Q) ∧R ⇔ (P ∧R) ∨ (Q ∧R) k) P ∧ (Q ∧R) ⇔ (P ∧Q) ∧R l)
P ⇒ Q ⇔ ¬P ∨Q m) ¬(P ⇒ Q) ⇔ P ∧ ¬Q n) P ⇒ P ⇔ true 1 • State on every line in the proof the axiom that you have used.
• No other axioms or inferences may be used. • For example, to prove (P ∨ false)⇔ P is true,
a solution is: (P ∨ false)⇔ P [ Premise ] ⇔ (P ⇔ P ) [ a ] ⇔ true [ n ] Submit the file ex123.pdf,
which should contain the solution to this exercise and ex1 and ex3. ex3 8 marks
The following code fragments show the pre- and post-conditions. Prove the code correct using the inference rules from lectures.
Indicate the rule that you use in each step. i {true} if x>y then m:=x else m:=y; {(m ≥ x) ∧ (m ≥ y)} ii {x = 2n} x:=x*2; n:=n+1; {x = 2n} iii {x = 2n ∧ (n ≤ p)} while n