def double(a):
    """returns a list  b  that holds all of  a's  values * 2 (see post)"""
    """{ pre  True
         post forall 0 <= i < len(a), b[i] == a[i] * 2
         return b
    }"""
    b = []
    x = 0
    """{ 1.OK forall 0 <= i < x, b[i] == a[i] * 2    foralli
         2.OK x == len(b)                 algebra
    }"""
    while x != len(a) :
        """{ invariant  (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b))
             modifies x, b
        }"""
        b.append(a[x]*2)
        """{ 1.OK (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b_old))  premise
             2.OK x == len(b_old)                         ande 1
             10.OK forall 0 <= i < x, b[i] == a[i] * 2    ande 1
             3.OK len(b) == len(b_old) + 1                 premise
             4.OK x == len(b)-1                                 algebra 2 3
             5.OK b[len(b)-1] == a[x]*2                    premise
             6.OK b[x] == a[x]*2                          subst 4 5
             7.OK forall 0 <= i < x+1, b[i] == a[i] * 2  foralli 10 6
             8.OK len(b) == x + 1                         algebra 4
             9.OK return 7 8
        }"""
        x = x + 1
        """{ 1.OK  forall 0 <= i < x_old +1, b[i] == a[i] * 2  premise
             2.OK  x == x_old +1                              premise
             3.OK forall 0 <= i < x, b[i] == a[i] * 2    subst 2 1
             4.OK len(b) == x_old + 1                       premise
             5.OK len(b) == x                             subst 2 4
             6.OK x == len(b)                             algebra 5
             #7.OK (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b)) andi 3 6
             8. return 3 6
        }"""

    """{ 1.OK (forall 0 <= i < x, b[i] == a[i] * 2) and (x == len(b))  premise
         3.OK not(x != len(a))                        premise
         4.OK x == len(a)                            algebra
         6.OK forall 0 <= i < x, b[i] == a[i] * 2    ande 1
         5.OK forall 0 <= i < len(a), b[i] == a[i] * 2   subst 4 6
    }"""
    return b