[[Property:title|New attribute layout]] [[Property:weight|4]] [[Property:uuid|b13c9004-c8a0-6628-5c70-42c3e2617c10]]
class
PRODUCT
feature {NONE} -- Access
price: DOUBLE
-- Cost in dollars.
feature -- Element change
set_price (a_price: DOUBLE)
-- Assign `a_price' to `price'.
require
a_price_non_negative: a_price >= 0.0
do
price := a_price
ensure
price_assigned: price = a_price
end
invariant
price_non_negative: price >= 0.0
end -- class PRODUCT