38 lines
593 B
Plaintext
38 lines
593 B
Plaintext
note
|
|
description: "Summary description for {ENUM}."
|
|
author: ""
|
|
date: "$Date$"
|
|
revision: "$Revision$"
|
|
|
|
deferred class
|
|
ENUM
|
|
|
|
feature -- Access
|
|
|
|
is_valid_state: BOOLEAN
|
|
-- Is the value of the enumeration valid?
|
|
do
|
|
Result := is_valid_value (value)
|
|
end
|
|
|
|
value: INTEGER
|
|
-- The current value of the enumeration.
|
|
|
|
set_value (a_value: INTEGER)
|
|
require
|
|
is_valid_value (a_value)
|
|
do
|
|
value := a_value
|
|
end
|
|
|
|
is_valid_value (a_value: INTEGER): BOOLEAN
|
|
-- Can `a_value' be used in a `set_value' feature call?
|
|
deferred
|
|
end
|
|
|
|
invariant
|
|
is_valid_state
|
|
|
|
end -- class ENUM
|
|
|