Убедитесь, что предложение в Eiffel касается синтаксиса

 find(c: CHARACTER; position: INTEGER): INTEGER

Эта функция находит символ, начиная с позиции i и выполняя поиск. Как только он находит индекс, он выводит его. Однако, если в слове такого символа нет, то выводится 0.

Вопрос: Постусловие должно утверждать, что запрос возвращает индекс символа c в слове в диапазоне pos .. word.count или ноль, если такого символа нет.

Мой код:

find(c: CHARACTER; position: INTEGER): INTEGER
   require
            .....
   do

            .....
   ensure 
        across word as w
        some
             (w.item = c and w.cursor_index >= position)
        end
   end

Проблема с этим логическим равенством заключается в том, что когда используется find (c, pos) и ничего не найдено, функция вызывает нарушение постусловия.

Я пытаюсь сделать так, чтобы функция выводила ТОЛЬКО, когда данный символ c не существует в слове


eiffel
person geforce    schedule 11.01.2016    source источник
comment
Я не уверен, что правильно понимаю вопрос, но для вашего постусловия вы можете сделать что-то вроде: Result = 0 или else (Result ›= position and word.at (Result) = c)   -  person Louis M    schedule 12.01.2016
comment
Нет, это не сработает, потому что я не могу выводить целые числа, оно принимает только логическое значение   -  person geforce    schedule 12.01.2016
comment
Тогда я не понимаю вашу функцию "найти". Он имеет тип результата INTEGER.   -  person Louis M    schedule 12.01.2016

Ответы (2)


arrow_upward
1
arrow_downward

Предполагая, что это должно быть полное постусловие, давайте рассмотрим проблему в каждом конкретном случае:

  1. В. Каков допустимый диапазон выходных значений?
    А. Результатом может быть 0 или любая допустимая позиция в word, начиная с position:

    valid_result_range: Result = 0 or position <= Result and Result <= word.count

    Здесь мы предполагаем, что position неотрицательно (надеюсь, это указано в предварительном условии).

  2. В. Какое будет выходное значение, если нет совпадающих символов?
    A. Выходное значение - 0. Все символы с индексами, начинающимися с position, не совпадают:

    zero_if_not_found: (Result = 0) =
    across word as wc all
        position <= wc.target_index implies wc.item /= c
    end

  3. В. Какое будет выходное значение, если есть соответствующий символ?
    A. Это первая позиция соответствующего символа, начиная с position:

    non_zero_if_found: (Result /= 0) implies
   (
      word [Result] = c
   and
      across word as wc all
         (position <= wc.target_index and w.target_index < Result) implies
         wc.item /= c
      end
   )

    Это постусловие состоит из двух частей. Проверяется, что персонаж найден. Другой проверяет, нет ли перед этой позицией совпадающих символов.
    РЕДАКТИРОВАТЬ: исходный код начинался с (Result /= 0) = ... вместо (Result /= 0) implies .... Это вызовет нарушение утверждения в word [Result], когда Result = 0. Код с implies свободен от этой проблемы, потому что если выражение до implies равно False, то выражение после него не оценивается.

Последнее постусловие - это комбинация всех приведенных выше утверждений. Порядок утверждений важен, потому что non_zero_if_found полагается на тот факт, что Result является допустимым индексом для word.

person Alexander Kogtenkov    schedule 12.01.2016
comment
Просто интересно, а зачем ставить wc.target_position ‹= word.count? Итератор делает это сам? - person geforce; 13.01.2016
comment
@GeForce цикл across проходит только через все допустимые индексы, поэтому нет необходимости проверять, является ли текущий индекс допустимым, в данном случае в диапазоне _2 _.._ 3_. - person Alexander Kogtenkov; 13.01.2016

arrow_upward
1
arrow_downward

Я бы немного изменил ответ Александра:

zero_if_not_found: (Result = 0) подразумевает ... non_zero_if_found: (Result / = 0) подразумевает ...

Чтобы понять, почему, рассмотрим, что происходит, когда Result = 0, и мы оцениваем non_zero_if_found Александра:

(Результат / = 0) оценивается как Ложь. Тогда слово [Результат] = c оценивается как сбой предварительного условия (действительный_индекс - я предполагаю, что слово имеет тип STRING). (замена w [Result] на слово [Result], поскольку это была опечатка Александра, я думаю)

Использование подразумевает защиту от этого, поскольку RHS не оценивается.

person user2783273    schedule 12.01.2016
comment
Действительно, в моем коде для non_zero_if_found была ошибка, теперь она исправлена. Что касается добавления implies к zero_if_not_found, мне кажется, что оставить равенство лучше, потому что тогда мы узнаем, когда Result равно 0 непосредственно из утверждения, и в этом случае безопасно использовать равенство. Спасибо! - person Alexander Kogtenkov; 12.01.2016
comment
OK. Похоже, target_position - очередная опечатка для target_index? - person user2783273; 13.01.2016