0

我正在开发一个用 Eiffel 语言编写的规划软件，我创建了以下代码，但我不太确定应该为此类的例程指定哪种后置条件和/或前置条件。

如果您可以为此提供语法提示，那就太好了，因为我不是埃菲尔语言的大师，而且以我目前的知识水平，它的关键字仍然有点棘手且难以理解。

class TIME
feature -- Initialization
 make (one_hour, one_min, one_sec: NATURAL_8)
 -- Setup ‘hour’, ‘minute’, and ‘seconds’ with
 -- ‘one_hour’, ‘one_min’, and ‘one_sec’, as corresponds.
 require
 do
 hour := one_hour
 minute := one_min
 second := one_sec
 ensure
 end
feature -- Setters
 set_hour (one_hour: NATURAL_8)
 -- Updates `hour' w/ value ‘one_hour’.
 require

 do
 hour := one_hour
 ensure

 end
 set_min (one_min: NATURAL_8)
 -- Updates `minute' w/ value ‘one_min’.
 require
 do
 minute := one_min
 ensure
 end
 set_sec (one_sec: NATURAL_8)
 -- Updates `second' w/ value ‘one_sec’.
 require
 do
 second := one_seg
 ensure
 end
feature -- Operation
 tick
 -- Counts a tick for second cycle, following 24 hr format
 -- During the day, “tick” works as follows
 -- For example, the next second after 07:28:59 would be
 -- 07:29:00. While the next second of 23:59:59
 -- is 00:00:00.
 do
 ensure
 end
feature -- Implementation
 hour: NATURAL_8
 minute: NATURAL_8
 second: NATURAL_8
invariant
 range_hour: hour < 24
 range_minute: minute < 60
 range_second: second < 60
end
4

2 回答 2

1

这是我会使用的：

对于构造函数：

make (one_hour, one_min, one_sec: NATURAL_8)
        -- Setup `hour', `minute', and `seconds' with
        -- `one_hour', `one_min', and `one_sec', as corresponds.
    require
        Hour_Valid: one_hour < 24
        Minute_Valid: one_min < 60
        Second_Valid: one_sec < 60
    do
        hour := one_hour
        minute := one_min
        second := one_sec
    ensure
        Hour_Assing: hour = one_hour
        Minute_Assing: minute = one_min
        Second_Assing: second = one_sec
    end

换句话说，前提条件表明参数在类的上下文中有效的要求是什么。您可能会想问，如果这些前提条件已经存在于不变量中，为什么还要放置这些前提条件。答案是：两者都不存在的原因相同。将不变量视为类必须（始终）有效的状态。唯一必须确保此不变量有效的是类本身或其后代（但不是类的客户端）。换句话说，make确保不变量有效的是特性的角色，而不是特性的调用者的角色make。这将我们带到我提出的前提条件的原因make。因为是的，这是make确保不变量得到尊重的作用，但是如果make想要尊重不变量，它必须限制客户端可以接收什么值作为参数。因此，换句话说，前提条件“Hour_Valid: one_hour < 24”确保特征“make”可以确保它可以尊重不变的“range_hour: hour < 24”。

现在，对于后置条件。当例程的第一行是 'hour := one_hour' 时，你会发现放置像 'Hour_Assing: hour = one_hour' 这样的后置条件很奇怪。关键是，如果我继承了该类TIME并更改了实现（例如，我使用时间戳，例如自一天开始以来的秒数），则后置条件的尊重不会那么微不足道，但是后置条件仍将适用于新make例程。您必须将这些（前置条件和后置条件）视为文档。这就像对功能的调用者说make，如果参数one_hour是有效的，我可以向你保证，无论实现是什么，它hour都等于和那个。one_hour

现在，我会为每个 setter 设置等效的前置条件和后置条件。例如：

set_hour (one_hour: NATURAL_8)
        -- Updates `hour' with the value ‘one_hour’.
    require
        Hour_Valid: one_hour < 24
    do
        hour := one_hour
    ensure
        Hour_Assign: hour = one_hour
    end

对于不变量，我认为您已经在代码中放入了好的不变量。所以我认为这里不需要更多的解释。最后，将每个合同（前置条件、后置条件和不变量）视为文档非常重要。这些必须是可选的，如果编译器将它们删除，则生成的程序必须等同于带有合同的程序。将其视为可以帮助您调试的代码文档。

于 2016-06-14T16:33:23.387 回答
0

我不是 Eiffel 方面的专家，我的经验主要来自 C# CodeContracts，但在这里。

我将为您的 set_hour 功能提供一个示例语法。希望您可以将其推广到整个示例：

 set_hour (one_hour: NATURAL_8)
 -- Updates `hour' w/ value ‘one_hour’.
 require
  -- generally you can put here any boolean expression featuring arguments/class variables
  hour_in_range: one_hour < 24 -- the part before : is optional, it's called
  -- a name tag, helps with debugging.
 do
  hour := one_hour
 ensure
  hour_is_set: hour = one_hour -- it may seem excessive, but for verification tool such as automated proovers this information is valuable. 
  hour < 24 -- this one duplicates your invariant, you may or may not want to add contracts like this, depending on your needs/style/etc.
于 2016-06-14T16:19:22.270 回答