1 Hoare triples Task 1.1 (Written, 10 points). Let s = while i < x do x := x * i; i := i + 1 od. For each of the following, is the triple satisfied or unsatisfied in the given state? Explain why by unfolding the definition as we saw in the class. Note that some of these are partial correctness triples and others are total correctness. a) {i = 1, x = 6} =[ i < x ] s [ i = x ] b) {i= -1, x = 5} = {i < x} s {i 0^x 0} c) {i=1, x = 0} = {i < x} s {i=x} d) {i=1,x=2} = {x = k} s {x = k!} e) {i = 1, x = 6} = {T} s {]k.x = k!} Task 1.2 (Written, 6 points). Consider program s in the previous task. For each of the following triples, say if it's valid (satisfied in all states or not). If not, provide a counterexample and then fix either the precondition, or the postcondition or the statement to make the triple valid. Don't make your change trivial (that is, don't make the precondition a contradiction, the postcondition a tautology or the statement soemthing that always errors or diverges). a) {T} s {x > 0} b) {x = k} s {x = k} c) [i=1^x=k^x>0] s[i= k^x=k! ] Task 1.3 (Written, 5 points). Fill in an appropriate precondition such that the following triple is valid. Don't provide a trivial precondition (that is, don't make the precondition a contradiction). [_ ] n := -m; while n 0 do r := r * 3; n := n 1 od [ r = 3m ] 1 Hoare triples Task 1.1 (Written, 10 points). Let s = while i < x do x := x * i; i := i + 1 od. For each of the following, is the triple satisfied or unsatisfied in the given state? Explain why by unfolding the definition as we saw in the class. Note that some of these are partial correctness triples and others are total correctness. a) {i = 1, x = 6} = [ i < x ] s [ i = x ] b) {i= -1, x = 5} = {i < x} s {i 0 ^x 0} c) {i = 1,x = 0} = {i < x} s {i = x} d) {i=1,x=2} = { x = k} s { x = k!} e) {i = 1, x = 6} = {T} s {]k.x = k!} Task 1.2 (Written, 6 points). Consider program s in the previous task. For each of the following triples, say if it's valid (satisfied in all states or not). If not, provide a counterexample and then fix either the precondition, or the postcondition or the statement to make the triple valid. Don't make your change trivial (that is, don't make the precondition a contradiction, the postcondition a tautology or the statement soemthing that always errors or diverges). a) {T} s {x > 0} b) {x = k} s { x = k} c) [i=1^x=k^x> 0 ] s[i= k^x=k! ] Task 1.3 (Written, 5 points). Fill in an appropriate precondition such that the following triple is valid. Don't provide a trivial precondition (that is, don't make the precondition a contradiction). [_ ] n := -m; while n 0 do r := r * 3; n := n 1 od [ r = 3m ]