Untitled

note
  description: "Objects that represent ADT MAP:KEY x VALUE."
  author: "Przemyslaw Pawluk"
  date: "2013 May 9"
  version: 1.0

class
    MY_MAP[K,V]
create
   make


feature {none}  --Representation

list:LINKED_LIST[ITEM[K,V]]


count: INTEGER -- counter


feature {ANY}

    make
        --creates all required variables
    do

    create list.make
    count:=0;

    ensure

         count = 0
         list.is_empty
    end


    put(key: K; value: V)
        --add the give <key, value> to the map. If the key already exist then the value is updated.

        require
          key_Nvoid: key /= void
          val_Nvoid: value /= void

        local
            i, j, capacity: INTEGER
            exit: BOOLEAN
            item: ITEM[K,V]
        do


           create item.make (key,value)
            capacity := count + 1
            i := 1
            j := count

--         if the key exist find the key. If not, simply add the key and val to the map.
           if has_key(key)
           then
                from
                list.start
                invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                           (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                           (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(0) is alwais = N
--                          NOT CODED: for all N elements in the map, the elements
--                          from 1 to i-1 does dont contain the key.

                until
--                 i starts at 1. Thus this condition will be true when i >= capacity (N + 1) or the key has been found, and exit the loop.
                   i >= capacity or exit
                loop


                    if   list.i_th (i).getkey ~ (key)
                    then
                        list.go_i_th (i)
                        list.replace (item)

                        exit := true -- exit loop


                    end

                    i := i + 1
                    j := j - 1
                    variant j

                end

            else

                  list.extend (item)
                  count := count + 1
            end

        ensure
--      ensure the key was added
        putWorked:  exist1 (key, value)

 --     if the key existed current count must equal old count
 --     if the key did not exist then current count must equal old count + 1
        correct_count: ( old current.has1(key) and count = old count) xor
                              (not old current.has1(key) and count = old count + 1)
        end


    get(key:K):V
    -- the key must exist in the map. return the value associated with the given key.
    require
        Key /= void
        has_key(key) -- PLEASE READ: The proffesor stated in class, if the key dosent exist, we can leave the resposibility to the user
                     --              by adding a requirement where the key passed must exist. thus, it is the users resposibility
                     --              to check if the key exist before he runs this method.


    local
         i,j, capacity : INTEGER
         exit : BOOLEAN
         item: ITEM[K,V]
         value: V
         value_void :  detachable V

    do
            capacity := count + 1
            i := 1
            j := count

            from
                list.start
            invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                       (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                       (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(0) is alwais = N
--                      not coaded: for all N elements in the map, the elements
--                      from 1 to i-1 does dont contain the key.
--
            until
--              i starts at 1. Thus this condition will be true when i >= capacity (N + 1) or the key has been found, and exit the loop.
                i >= capacity or exit
            loop
                if   list.i_th (i).getkey ~ key
                then

                    value := list.i_th (i).getvalue
--                  so we dont return the reference
                    result := value.deep_twin

                    exit := true -- exit loop

                end

                i := i + 1
                j := j - 1

                variant j
--
                end

--          PLEASE READ:  this is how I would make my method return a void value if required.

--          if (not exit)
--          then

--              result := value_void
--          end


        ensure

            no_change_attributes: no_change_attributes (old count, old key_set, old value_set)

            correct_output: exist1(key, result)
--          PLEASE READ: if void is allowed to be returned then my method would have the following ensure:
--          correct_output: ( not current.has_key(key) and result = void) xor
--                              ( current.has_key(key) and exist1(key, result))

    end

    remove(key:K)
--  given key is removed from the map.
    require
        void_key:  key /= void

    local
    i,j, capacity : INTEGER
    stop: BOOLEAN

    do
        capacity := count + 1
        i := 1
        j := count


            from
                list.start
            invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                       (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                       (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(0) is alwais = N
--                      not coaded: for all N elements in the map, the elements
--                      from 1 to i-1 does dont contain the key.
--
            until
--              i starts at 1. Thus this condition will be true when i >= capacity (N + 1) or the key has been found, and exit the loop.
                i >= capacity or stop
            loop
                if
                    list.i_th (i).getkey ~ key
                then
                    list.go_i_th (i)
                    list.remove
--                  one item has been removes thus the map count must decrement by 1
                    count := count - 1
                    stop := true -- exit loop
                end
                i := i + 1
                j := j - 1
                variant j

--          end

        end

        ensure
--          1) if the key existed in the map ensure the count has been decrented by 1 and the key has actualy been removed
--          2) if the key does not exist ensure no changes have been made to the map.
--          3) "xor" only one of conditions 1 or 2  can be true at the same time.
           correct_remove: old has_key (key) and old count - 1 = count and not has_key(key) xor
           not old has_key(key) and no_change_attributes (old count, old key_set, old value_set)


    end

    has(key:K; val:V):BOOLEAN
    -- returns true if the given combination of the key and value exist in the map
    -- does not guarantee there exist only one combination of the given key and value
    require
        void_key: key /= void
        void_val: val /= void


    local
        i,j, capacity : INTEGER
        return : BOOLEAN
    do
        capacity := count + 1
        i := 1
        j := count

        from
             list.start
        invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                   (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                   (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(0) is alwais = N
--                  not coaded: for all N elements in the map, the elements
--                  from 1 to i-1 does dont contain the given combination of key and value.
        until
--           i starts at 1. Thus this condition will be true when i >= capacity (N + 1) or the combination of the key and value has been found. exit loop.
             i >= capacity or return
        loop
--          check if the given combination of key and value match the key and value at the i th location
            if   (list.i_th (i).getkey ~ key) and (list.i_th (i).getvalue ~ val)
            then
               return := true
            end
            i := i + 1
            j := j - 1
            variant j
        end


        result := return
        ensure
--          ensure no changes has been made to the map
            no_change: no_change_attributes (old count, old key_set, old value_set)

--          use exist(K,V) to ensure that has(K,V) returned the correct result
            correct_out: result = exist(key, val)

    end
--------------------------------------------------------------------------------------------------
    key_set:SET[K]
    -- returns a set of key values from the map
    local
        set: LINKED_SET[K]
        i,j, capacity : INTEGER
    do
        capacity := count + 1
        i := 1
        j := count
        create set.make
        from
            list.start
        invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                   (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                   (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(N - N) is alwais = N
        until
--           i starts at 1. Thus this condition will be true when i >= capacity (N + 1)
            i >= capacity
        loop
--          add a copy of the key to the set
            set.extend (list.i_th (i).getkey.deep_twin)

            i := i + 1
            j := j - 1
        variant j

        end
        result := set


        ensure
--      ensure all the keys from the map where added to the list
        containAllKey_set:  current.key_check(result)

--      ensure no changes where made to the map
        no_change: no_change_attributes (old count, old key_set, old value_set)

    end

    value_set:SET[V]
    -- returns a set of values from the map

    local
        i,j, capacity : INTEGER
        set: LINKED_SET[V]

    do

        capacity := count + 1
        i := 1
        j := count
        create set.make
        from
            list.start
        invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                   (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                   (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(N - N) is alwais = N
        until
--           i starts at 1. Thus this condition will be true when i >= capacity (N + 1)
            i >= capacity
        loop
--              add a copy of the key to the set
                set.extend (list.i_th (i).getvalue.deep_twin)
                i := i + 1
                j := j - 1
        variant j

        end

        result := set


        ensure
--      ensure all the values from the map where added to the list.
        no_change: no_change_attributes (old count, old key_set, old value_set)
--      ensure no changes where made to the map
        containAllVal_set:  current.val_check(result)

    end

feature --Quantifiers

    exist(key:K; val:V):BOOLEAN
    --checks if given key/value combination exist in the map
   -- does not guarantee there exist only one combination of the given key and value
    require
        key /= void
        val /= void
    local
        i,j, capacity: INTEGER
        exit: BOOLEAN
        return: BOOLEAN
    do
        capacity := count + 1
        i := 1
        j := count
        return := false
        from
            list.start

        invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                   (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                   (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(0) is alwais = N
--                  not coaded: for all N elements in the map, the elements
--                  from 1 to i-1 does dont contain the given combination of key and value.

        until
--          i starts at 1. Thus this condition will be true when i >= capacity (N + 1) or the combination of the key and value has been found. exit loop.
            i >= capacity or exit
        loop
--          check if the given combination of key and value match the key and value at the i th location
            if (list.i_th (i).getkey ~ key) and (list.i_th (i).getvalue ~ val)
            then
                return := true
                exit := true
            end
            i := i + 1
            j := j - 1
            variant j
        end
        result := return

        ensure
--      ensure no changes where made to the map
         no_change: no_change_attributes (old count, old key_set, old value_set)
    end
feature
    exist1(key:K; val:V):BOOLEAN
    --checks if there is only one pair with given key/value combination
    require
        key /= void
        val /= void
    local
        i,j, capacity: INTEGER
        count_in: INTEGER
    do
        capacity := count + 1
        i := 1
        j := count
        from
            list.start
        invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                   (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                   (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(0) is alwais = N

        until
--          i starts at 1. Thus this condition will be true when i >= capacity (N + 1)
            i >= capacity
        loop
--          check if the given combination of key and value match the key and value at the i th location
            if list.i_th (i).getkey ~ key and list.i_th (i).getvalue ~ val
            then
--              keep count of how many times this block is accessed
                count_in := count_in + 1
            end

            i := i + 1
            j := j - 1
            variant j
        end

--      if count = 1 then the block was only accesed once and there is only one matching key and value in the map
        if count_in = 1
         then
            result := true
        else
            result := false
        end

        ensure
--          ensure no changes have been made to the map
            no_change: no_change_attributes (old count, old key_set, old value_set)
    end

    has1(key:K):BOOLEAN

    --checks if there is only one key with given value
    require
        key /= void
    local
        i,j, capacity: INTEGER
        count_in: INTEGER
    do
        capacity := count + 1
        i := 1
        j := count
        count_in := 0
        from
            list.start
        invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                   (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                   (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(0) is alwais = N

        until
--          i starts at 1. Thus this condition will be true when i >= capacity (N + 1)
            i >= capacity
        loop

            if key ~ list.i_th (i).getkey
             then
--              keep count of how many times this block is accessed
                count_in := count_in + 1
            end

            i := i + 1
            j := j - 1
            variant j

        end
--      if count = 1 then the block was only accesed once and there is only one matching key in the map
        if (count_in = 1)
         then
            result := true
        else
            result := false
        end


        ensure
            no_change: no_change_attributes (old count, old key_set, old value_set)
    end
--------------------------------------------------------------------------------------------------------
--------------------------------------------------------------------------------------------------------
feature -- map method's testers for ensure
    has_key(key:K):BOOLEAN
--  checkes if the given key is in the map
    require
        key /= void
    local
        i,j, capacity: INTEGER
        return : BOOLEAN
    do
        capacity := count + 1
        i := 1
        j := count
        return := false
        from
            list.start

        invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                   (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                   (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(0) is alwais = N
--                  not coaded: for all N elements in the map, the elements
--                  from 1 to i-1 does dont contain the given combination of key and value.
        until
--          i starts at 1. Thus this condition will be true when i >= capacity (N + 1). exit loop
               i >= capacity
        loop

            if (list.i_th (i).getkey ~ key)
            then
                 return := true
            end
                i := i + 1
                j := j - 1
            variant j
        end

            result := return
        ensure
--          no changes have been made to the map
            no_change: no_change_attributes (old count, old key_set, old value_set)
    end
feature{MY_MAP}
    key_check(set1: SET[K]):BOOLEAN
    -- to check if every key is in the set

    require
--      key_same_size: set1.count = count
    local
        i,j, capacity: INTEGER
        exit: BOOLEAN
    do
        capacity := count + 1
        i := 1
        j := count
        exit := false


        from
            list.start
        invariant ((i <= capacity) and -- let N be the number of elements in the map. and i be the number of iterations. for all i such that i(1), i(2)... i(N). i is always <= N
                   (j >= 0) and -- for all j such that j(N - 1), j(N - 2)... j(0). j is always >= 0
                   (i + j = capacity))-- for all i and j such that j(N - 1)+ i(1), i(2) + j(N - 2)... i(N)+j(0) is alwais = N
--                 not coaded:  let i be the location of the present iteration. Then for all N elements in the map and  K be the elements in the Set, such that
--                  N(1) = K(1), N(2) = K(2)..... N(i-1) = k(i - 1).

        until
            i >= capacity or exit
        loop
            set1.compare_objects

--          if any items in the set dont match the item in the list then we exit loop
            if set1.has (list.i_th (i).getkey)
            then
            exit := false
            else
            exit := true
            end
            i := i + 1
            j := j - 1
            variant j
        end
        -- if exit is true, loop was exited
        -- one key of the list is not in the set, result := false
        result := not exit


        ensure
         no_change: no_change_attributes (old count, old key_set, old value_set)

    end

     val_check(set1: SET[V]):BOOLEAN
    -- to check if every val is in the set
    require
--      val_size: set1.count <= count -- SET does not allow duplicates, so  ensure that set count is always <= map count
    local
        i,j, capacity: INTEGER
        exit: BOOLEAN
    do
        capacity := count + 1
        i := 1
        j := count

        from
            list.start

        invariant ((i <= capacity) and -- let K be the number of elements in the set. and i be the number of iterations 1 to K. for all i such that i(1), i(2)... i(K). i is always <= K <=N
                   (j >= 0) and -- for all j such that j(K - 1), j(K - 2)... j(K - K). j is always >= 0
                   (i + j = capacity))-- for all i and j such that j(K - 1)+ i(1), i(2) + j(K - 2)... i(K)+j(K-K) is alwais = K
--                  let i be the location of the present iteration from 1 to K.  K being the # of set elements and N the number of
--                  elements in the map, such that N(1) = K(1), N(2) = K(2)..... N(i-1) = k(i - 1).
--
        until
            i >= capacity or exit
        loop

            set1.compare_objects
            if set1.has (list.i_th (i).getvalue)
            -- if the value value is not in the set. exit the loop.
            then
            exit := false
            else
            exit := true
            end
            i := i + 1
            j := j - 1
            variant j
        end
        result := not exit
        -- if exit is true, loop was exited
        -- one key of the list is not in the set, result := false

        ensure
         no_change: no_change_attributes (old count, old key_set, old value_set)

    end

    no_change_attributes( old_count : INTEGER
                    ; old_keys : SET[K]; old_values : SET[V]) : BOOLEAN
         do
            Result := count = old_count and deep_equal(key_set, old_keys)
                  and deep_equal(value_set, old_values)

         end


invariant
    count: count>=0
    correct_count: count = list.count
    key_set.count = count

    -- for all elements in the list there exist a unique key
    unique_keys: across list as l all
                    has1(l.item.getkey)
     end

end