为什么我在埃菲尔中得到了valid_index先决条件违规？

我只是简单地测试一个容器类的push_at特性（基本上是由数组产生的）。我不知道我的代码的哪一部分触发了这种违规行为。为什么我在埃菲尔中得到了valid_index先决条件违规？

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

感谢您的帮助！

来源

2017-09-22 Mzzz

它是容器[i]。当你创建con时，它将是空的（可能 - 你没有向我们展示你的代码）。您的先决条件需要反映con []的先决条件。这又需要反映{ARRAY} .put的前提条件，您必须使用它来实现它。你目前的先决条件不会这样做（这是相当随意的）。

来源

2017-09-23 07:32:48 user2783273

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

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

（在你的榜样属性container）用于存储不同的结构，例如它可能是HASH_TABLE [STRING, INTEGER]。然后可以将元素存储在任意索引处。
确保存储是预先分配的。如果您知道可能的索引范围，则可以初始化container以从头开始使用它们。它可以使用create container.make_filled ("", 1, N)创建，其中N是最大索引。（我假设container的类型为ARRAY [STRING]。）
逐个添加元素。在这种情况下的push_at前提应该检查所提供的索引是否要么存在或邻近先前分配的一个：
```
require 
     valid_index: i >= 1 
     existing_or_adjacent_index: 
      container.valid_index (i) or else 
      container.valid_index (i - 1) 
```
的push_at代码应适于使用将分配，如果一个新的索引的特征随机提供的超出分配的索引范围：
```
container.force (s, i) 
```

化妆品：没有必要重复在创建指令create {CONTAINER} con.make类型声明，因为变量012的类型是CONTAINER。所以，使用create con.make就足够了。

来源

2017-09-23 11:49:49

谢谢。我忘了增加容器。问题解决了。 – Mzzz

为什么我在埃菲尔中得到了valid_index先决条件违规？

回答

相关问题