AutoFix: Fixing the Implementation

Figure 1.a shows a faulty routine in class TWO_WAY_SORTED_SET. The routine move_item takes an argument v, which must be a non-Void element stored in the set, and moves it to the position to the left of the internal cursor (attribute index). To this end, the routine saves the cursor position into a local variable idx, moves index to where v occurs in the set, removes this occurrence of v, restores index to its initial position, and inserts v to the left of the cursor. The implementation shown fails with a violation of go_i_th(idx)'s precondition whenever the internal cursor initially points to the last valid cursor position count + 1 (see Figure 2). In fact, the removal of one element in the set invalidates the position stored in idx, expressible as count + 2 with respect to the value of count after removal. A closer look reveals that the routine is incorrect even in cases when this precondition violation does not occur: if v appears to the left of the internal cursor initially, the sequence of operations moves v to an incorrect "off-by-one" position. Figure 1.b shows a fix suggested by AutoFix; the fix corrects the routine even for the cases when it does not trigger a precondition violation invoking go_i_th(idx).

  move_item (v: G)
            -- Move `v' to the left of cursor.
        require

            v /= Void
            has (v)
        local

            idx: INTEGER
            found: BOOLEAN
        do
            idx := index
            from start until found or after loop
                found := (v = item)
                if not found then forth end
            end
            check found and not after end
            remove
            
            go_i_th (idx)
            put_left (v)
        end

      go_i_th (i: INTEGER) require 0 <= i <= count + 1
      put_left (v: G) require not before
      before: BOOLEAN do Result := (index = 0) end

  move_item (v: G)
            -- Move `v' to the left of cursor.
        require

            v /= Void
            has (v)
        local

            idx: INTEGER
            found: BOOLEAN
        do
            idx := index
            from start until found or after loop
                found := (v = item)
                if not found then forth end
            end
            check found and not after end
            remove
            if index < idx then idx := idx - 1 end
            go_i_th (idx)
            put_left (v)
        end

      go_i_th (i: INTEGER) require 0 <= i <= count + 1
      put_left (v: G) require not before
      before: BOOLEAN do Result := (index = 0) end

(a) Faulty routine (b) Fixed routine

Figure 1. A real fault from TWO_WAY_SORTED_SET.move_item

Figure 2. The effect of calling remove in move_item when index = count + 1 and after hold initially:
the following invocation of go_i_th(idx) triggers a precondition violation.