Consider the following imperative programming language: Px:=x=xx[P;P]w[x]P::=ab where P and x are non-terminal symbols that denote programs and variables, respectively, and a, b, w, =,,[,;, and ] are terminal symbols. Each of the variables a and b holds an integer value. Their initial values are given from outside of a program before execution. The semantics of each syntax is as follows. x1=x2x3 replaces the value of x1 with the integer obtained by subtracting the value of x3 from that of x2. [P1;P2] executes P1 and P2 sequentially in this order. w [x]P iterates P until the value of x is less than or equal to zero. Let A and B be propositions on the values of the variables. We say {A}P{B} if, whenever A holds before the execution of P,B holds at the time when P terminates. We say {A}P{B} if {A}P{B} is obtained just by a combination of the following rules: Rule 1 When P is of the form x1=x2x3, if A is literally identical to the proposition obtained by replacing every occurrence of x1 in B with the expression x2x3, then {A}P{B}. Rule 2 When P is of the form [P1;P2], if there exists a proposition C such that {A}P1{C} and {C}P2{B}, then {A}P{B}. Rule 3 When P is of the form w[x]P, if {A and x>0}P{A}, then {A}P{A and x0}. Rule 4 When there exist two propositions C and D such that C is a necessary condition for A, and D is a sufficient condition for B, if {C}P{D}, then {A}P{B}. For example, {a0} w [a] [a=a-a] {a=0} holds because 1. {aa0}a=aa{a0} (Rule 1), 2. {a0 and a>0}a=aa{a0} (Rule 4), 3. {a0} w [a][a=aa]{a0 and a0} (Rule 3 ), and 4. {a0} w [a][a=aa]{a=0} (Rule 4). Let F be the program w[a][a=ba;b=ba]. Answer the following questions. (1) Draw the syntax tree of F such that all the terminal symbols in F occur in its leaves. (2) Execute F with initial values (a,b)=(23,41) and calculate the values of a and b at the time when F terminates. (3) Show for some integer i,i0 and (ab)=(0111)i(01)}F{b=1}. (4) Determine whether or not F terminates for any initial values of a and b. Justify your