# 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