为什么我在Eiffel中遇到valid_index前置条件冲突？

Question

push_at (i: INTEGER; s: STRING)

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

    end

在我的测试仪中

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

谢谢你的帮助！

Answer 1

它是容器i。当你创建con时，它将是空的(可能-你还没有给我们展示你的代码)。您的前置条件需要反映con []上的前置条件。它反过来需要反映{.put}数组上的前提条件，您必须使用它来实现它。您当前的前提条件不能做到这一点(这是相当随意的)。

Answer 2

用作元素存储的底层结构不会自动为新元素分配内存。有些结构会在执行赋值器命令container [i] := s时执行此操作。但在您提到的代码中，情况并非如此。因此，此命令中使用的索引i无效，因此违反了前提条件。如果您查看异常跟踪或调用堆栈，您将看到前提条件违规不是发生在功能{CONTAINER}.puch_at中，而是发生在{ARRAY}.put或类似的地方，由于巧合和命名约定，它们使用相同的前置条件标记valid_index。

有不同的方法来解决这个问题：

1. 使用不同的存储结构(示例中的属性container )，例如，它可以是HASH_TABLE [STRING, INTEGER]。这样就可以在任意索引下存储元素了。
2. 会确保存储空间是预先分配的。如果您知道可能的索引的范围，那么可以将container初始化为从头开始使用所有索引。可以使用create container.make_filled ("", 1, N)创建，其中N是最大索引。(我假设container的类型是ARRAY [STRING].)
3. Add -by-one。在这种情况下，push_at的前提条件应该检查提供的索引是否存在，或者是否与先前分配的索引相邻：

需要valid_index: I >= 1 existing_or_adjacent_index: container.valid_index (i)或container.valid_index (i - 1)

push_at的代码应该调整为使用这样的功能:如果提供的索引超出已分配的索引范围，则会分配新的索引：

container.force (s，i) (s，i)

化妆品:不需要重复创建指令create {CONTAINER} con.make中的类型声明，因为变量con的类型是CONTAINER。所以，使用create con.make就足够了。