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). Updated 10/4: Added minus sign to postcondition n := -m; while n0 do r := r * -3; n := n - 1 od [r = 3-m ] Task 1.4 (Written, 3 points). = Write a precondition P such that the triple = [P] x sqrt(x)/y [T] is valid. Don't make your precondition trivial (a contradiction). Explain by unfolding the definition of the triple as we saw in the class. Task 1.5 (Written, 8 points). a) Write a program S and a precondition P2 such that # [P2]S2[T]. Explain by unfolding the defi- nition of the triple as we saw in the class. b) Have you used a while clause in S? If yes, can you provide another S this time without using the while clause? If no, can you provide another S this time with using the while clause? Task 1.6 (Written, 8 points). 2 a) Write a triple for the following program that is valid if and only if the program terminates when the initial value of x is greater than three. while x > 1 do if even(x) then x := 5x + 1 else x := x/2 fi od b) Write another triple for the above program which is valid if and only if the program does not terminate when the initial value of x is less than or equal to three.