CODEWITHSUNDEEP
eiffelpreconditions
buzzmind
buzzmind

Reputation: 109

Why I got valid_index precondition violation in Eiffel?

I just simply test a push_at feature of container class(made by array, basically). I dont know which part of my code triggers this violation.

push_at (i: INTEGER; s: STRING)

    require
        valid_index: i  >= 1
    do
        container [i] := s

    end

In my tester 

local
        con: CONTAINER

do
          create {CONTAINER}con.make
          con.push_at (1,"A")
          con.push_at (2,"B")

 Result := con.get(1) ~ "A" and con.get(2) ~ "B"
 check Result end
 end

Thanks for the help!

Upvotes: 1

Views: 305

Answers (2)

Alexander Kogtenkov
Alexander Kogtenkov

Reputation: 5810

The underlying structure used as a storage for the elements does not automatically allocate memory for new elements. Some structures do that when the assigner command container [i] := s is executed. But this is not the case in the code you mention. Consequently, the index i used in this command is invalid, hence the precondition violation. If you look at the exception trace or the call stack, you'll see that the precondition violation occurs not in the feature {CONTAINER}.puch_at, but in {ARRAY}.put or similar, which – by coincidence and naming convention – uses the same precondition tag valid_index.

There are different ways to solve the issue:

  1. Use a different structure for storage (the attribute container in your example), e.g. it could be HASH_TABLE [STRING, INTEGER]. Then it becomes possible to store elements at arbitrary indexes.

  2. Make sure the storage is pre-allocated. If you know the range of possible indexes, then container can be initialized to use them all from the beginning. It can be created with create container.make_filled ("", 1, N), where N is the maximum index. (I assume that container is of type ARRAY [STRING].)

  3. Add elements one-by-one. In this case the precondition of push_at should check whether the supplied index either exists or is adjacent to the previously allocated one:

    require
      valid_index: i >= 1
      existing_or_adjacent_index:
          container.valid_index (i) or else
          container.valid_index (i - 1)

    The code of push_at should be adapted to use the feature that will allocate a new index if the supplied one is beyond the range of allocated indexes:

    container.force (s, i)

Cosmetics: there is no need to repeat the type declaration in the creation instruction create {CONTAINER} con.make because the type of the variable con is CONTAINER. So, it's sufficient to use create con.make.

Upvotes: 0

user2783273
user2783273

Reputation: 91

It's container [i]. When you create con, it will be empty (probably - you haven't shown us your code). You precondition needs to reflect the precondition on con []. Which will in turn need to reflect the precondition on {ARRAY}.put, which you must be using to implement it. Your current precondition does not do that (it is rather arbitrary).

Upvotes: 0

Related Questions