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

此功能通过从位置 i 开始并搜索来查找字符。一旦找到索引，它就会输出它。但是，如果单词中不存在这样的字符，则输出 0

问题： 后置条件必须断言查询返回字符 c 在 pos .. word.count 范围内的 word 中的索引，如果没有这样的字符，则返回零。

我的代码： 

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 字符时才允许该功能输出

4

2 回答 2

1

假设它应该是一个完整的后置条件，我们逐案来看问题：

  1. Q. 允许的输出值范围是多少？
    A. 结果可以是或从 开始的0任何有效位置：wordposition

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

    在这里，我们假设它position是非负的（希望这是在前提条件中指定的）。

  2. Q. 如果没有匹配的字符，输出值是多少？
    A. 输出是0。索引从 开始的所有字符position都不匹配：

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

  3. Q. 如果有匹配的字符，输出值是多少？
    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]when中的断言违反Result = 0。带有impliesif 的代码不存在此问题，因为如果之前的表达式implies是False之后的表达式，则不会对其进行评估。

最后的后置条件是上述所有断言的组合。断言的顺序很重要，因为non_zero_if_found依赖Result于word.

于 2016-01-12T04:40:06.750 回答
1

我会稍微改变亚历山大的回答：

zero_if_not_found: (Result = 0) 暗示... non_zero_if_found: (Result /= 0) 暗示...

要了解原因，请考虑当 Result = 0 时会发生什么，并且我们评估 Alexander 的 non_zero_if_found：

(Result /= 0) 评估为 False 然后 word [Result] = c 评估为先决条件失败（valid_index - 我假设 word 是 STRING 类型）。（将 w [Result] 更改为单词 [Result]，因为这是 Alexander 的错字，我认为）

使用隐含可以保护您免受这种情况的影响，因为不会对 RHS 进行评估。

于 2016-01-12T08:24:01.547 回答