scottgw/language-eiffel — Issue #9: Attribute contracts
Author: nadia-polikarpova
Created: 2012-02-25 15:57:50+00:00
State: open

Attributes are allowed to have pre- and postconditions if they are marked with the "attribute" keyword.

Example:
version: NATURAL_32
-- Current version.
note
option: transient
attribute
ensure
definition: Result = 0
end
Found in: FLAT_INDEXABLE_ITERATION_CURSOR