Eiffel Contracts疑念

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

私は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. 

ここ

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を継承し、実装を変更した場合（例として、最初の日から2番目のタイムスタンプを使用します）、事後条件の尊重はそれほど簡単ではありませんが事後条件は新しい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 

不変量の場合、あなたはあなたのコードに既に良いものを入れていると思います。だからここで私は思う以上の説明は必要ない。終了するには、すべての契約（前提条件、事後条件および不変条件）を文書化することが非常に重要です。これらはオプションでなければならず、コンパイラーがそれらを削除する場合、結果のプログラムは契約書のものと同等でなければなりません。デバッグに役立つコードのドキュメントが好きです。