SENG 2011 Assignment 1 Predicate and Hoare Logic and Program Verification Due Sunday 9pm, 17th October, 2021 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