埃菲尔合同质疑答案

【问题标题】：Eiffel Contracts doubts埃菲尔合同质疑
【发布时间】：2016-06-14 15:25:58
【问题描述】：

我正在开发一个用 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

【问题讨论】：

那么，您的问题到底是什么？您在制定合同或用埃菲尔表达合同时遇到问题吗？
是的，我在用 Eiffel 表示它们时遇到问题，因为不明白必须使用哪种语法表达式、关键字等以及按什么顺序，我有一本书但没有足够的时间仔细看，老板催我尽快生成新代码。

标签： project-organization eiffel application-planning

【解决方案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

现在，对于后置条件。当例程的第一行是 '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

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

【讨论】：

【解决方案2】：

我不是 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.

【讨论】：