# speed_pldi09_fig4_2 # C4B: no bound ticks # eocimp: def startFig4_2(): var i, n, m, dir assume 0 < m assume m < n i = m while [0 < m and m < n] 0 < i and i < n: tick 1 if dir = 1: i = i + 1 else: i = i - 1