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

Question

 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 не существует в слове

Answer 1

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

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

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

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

2. В. Каково выходное значение, если нет соответствующих символов?
   А. Выход 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,

Answer 2

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

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

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

(Result / = 0) оценивается как False. Тогда слово [Result] = c приводит к ошибке предусловия (valid_index - я предполагаю, что слово имеет тип STRING). (я думаю, что вместо w [Result] на слово [Result] это опечатка Александра)

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