Weakest Preconditions - for Gina

   P:        { F1=F1SAVE & F1 < 256 & LOW < 256 }
   W1:       LDX 8
   W2:       LDA 0
   W3: LOOP  ROR F1
   W4:       BCC ZCOEF
   W5:       CLC
   W6:       ADC F2
   W7: ZCOEF ROR A
   W8:       ROR LOW
   W9:       DEX
   W10:      BNE LOOP
   Q:        { LOW + A*256 == F1SAVE*F2 }
In the above, the postcondition that is intended to be proved given P is Q. This can be done by finding the weakest w.r.t. Q at W1 and then showing that W1 equals T under the conditions of P. But W1 is not a predicate - it is a defun that is expressed in terms of the defun W7. The assignment is to find W7. The form W7 takes is the following:
   (defun W7 (F1 LOW A X C Z)
      (if (..some condition..)
          (..some value..)
          (W7 ..new F1.. ..new LOW.. ..new A.. ..new X.. ..new C.. ..new Z..)))
The reason for the arguments is they are all variables whose values change at some point during the multiply operation. The ..some condition.. should state the condition by which the loop terminates in terms of F1, LOW, A, X, C, Z (hint: but it should only depend on Z). The ..some value.. should be the result of the loop after termination and should somehow reflect the postcondition Q. The ..new F1.. etc. are obtained by substitution in a manner similar to what was done for W3 in terms of W7 in the assignment. As a check, the value for ..new F1.. is:
     (+ (* (MOD LOW 2) 128) (FLOOR F1 2))
which differs from the ..new F1.. of W3 in terms of W7 only by C being replaced with (MOD LOW 2).