Eiffel Contracts Zweifel

Question

Ich arbeite an einer Planungssoftware, die in Eiffel Sprache codiert ist, ich habe den folgenden Code erstellt, aber ich bin nicht ganz sicher, welche Art von Postbedingungen und/oder Vorbedingungen für diese Klasse angegeben werden sollten ' Routinen.

Wenn Sie Syntax Hinweise für diese geben können, wäre es toll, weil ich kein Meister in Eiffel Sprache bin, und seine Schlüsselwörter sind immer noch ein wenig schwierig & für mich bei meinem derzeitigen Kenntnisstand zu verstehen.

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

Ich bin kein Experte in Eiffel, meine Erfahrung kommt meist aus # CodeContracts C, aber hier geht es.

Ich werde nur eine Beispiel-Syntax für Ihre Funktion set_hour bieten. Hoffentlich können Sie diese auf Ihr gesamtes Beispiel verallgemeinern:

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

Hier ist, was ich verwenden würde:

Für den Konstruktor:

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 

Mit anderen Worten zeigt die Voraussetzungen, was Voraussetzung ist, damit die Argumente im Kontext der Klasse gültig sind. Sie könnten versucht sein zu fragen, warum diese Voraussetzungen gegeben sind, wenn diese bereits in den Invarianten enthalten sind. Die Antwort ist: Beide sind nicht aus dem gleichen Grund da. Sehen Sie eine Invariante als den Zustand, den eine Klasse (immer) haben muss, um gültig zu sein. Der einzige, der sicher sein muss, dass diese Invariante gültig ist, ist die Klasse selbst oder ihr Nachkomme (aber nicht der Client einer Klasse). Mit anderen Worten, es ist die Rolle des Merkmals make, sicher zu sein, dass die Invariante gültig ist, und nicht die Anrufer des Merkmals make. Das bringt uns zum Grund der Vorbedingung, die ich auf make setze. Denn ja, es ist die Aufgabe von make sicher zu sein, dass die Invarianten respektiert werden, aber wenn make die Invarianten respektieren wollen, muss es den Client einschränken, welchen Wert er als Argumente erhalten kann. Mit anderen Worten, die Vorbedingung 'Hour_Valid: one_hour < 24' stellt sicher, dass das Merkmal `make 'sicher sein kann, dass es die invariante' range_hour: hour < 24 'respektieren kann.

Jetzt für die Nachbedingung. Sie können es seltsam finden, eine Nachbedingung wie 'Hour_Assing: hour = one_hour' zu setzen, wenn die erste Zeile der Routine 'hour: = one_hour' ist. Der Punkt ist, wenn ich die Klasse TIME vererbe und ich die Implementierung ändere (zum Beispiel verwende ich einen Zeitstempel wie die Anzahl der Sekunden seit dem Anfang des Tages), wird der Respekt der Nachbedingung nicht so trivial sein, aber Die Nachbedingung gilt weiterhin für die neue Routine make. Sie müssen diese (Vorbedingung und Nachbedingung) als Dokumentation sehen. Es ist so, als würde ich den Anrufern des Features make sagen, dass, wenn das Argument one_hour gültig ist, ich Ihnen garantieren kann, dass hour gleich one_hour ist und das, wie auch immer die Implementierung sein mag.

Jetzt würde ich äquivalente Vorbedingung und Nachbedingung zu jedem Setter setzen. Zum Beispiel:

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 

Für die Invarianten denke ich, dass Sie bereits gute in Ihrem Code setzen. Also sind hier keine weiteren Erklärungen nötig. Abschließend ist es sehr wichtig, jeden Vertrag (Vorbedingungen, Nachbedingungen und Invarianten) als Dokumentation zu sehen. Diese müssen optional sein und wenn der Compiler sie entfernt, muss das resultierende Programm dem mit den Verträgen entsprechen. Sehen Sie es als Codedokumentation an, die Ihnen beim Debuggen helfen kann.