埃菲尔合同怀疑

Question

我正在编写一个以埃菲尔语言编写的计划软件，我创建了下面的代码，但我不太确定应该为这个班级指定哪种后置条件和/或前提条件“例程。

如果你能为此提供语法提示，那将会很棒，因为我不是埃菲尔语言的主人，而且它的关键字仍然有点棘手&在我目前的知识水平下很难理解。

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 

Answer 1

我不是埃菲尔的专家，我的经验大部分来自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. 

Answer 2

这里是我会用什么：

对于构造：

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，并且无论实施可能如何。

现在，我会把等同的先决条件和后置条件给每个制定者。例如：

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 

对于不变量，我认为你已经在你的代码中放好了。所以我认为在这里不需要更多的解释。要完成，将每个合同（先决条件，后置条件和不变量）视为文档非常重要。这些必须是可选的，如果编译器将其删除，则生成的程序必须与具有合同的程序相同。请参阅代码文档，以帮助您进行调试。