埃菲爾合同懷疑

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 

對於不變量，我認爲你已經在你的代碼中放好了。所以我認爲在這裏不需要更多的解釋。要完成，將每個合同（先決條件，後置條件和不變量）視爲文檔非常重要。這些必須是可選的，如果編譯器將其刪除，則生成的程序必須與具有合同的程序相同。請參閱代碼文檔，以幫助您進行調試。