indexing
description: "Transactions consisting out of a single transfer"
status: "See note at end of class"
date: "$Date$"
revision: "$Revision$"
class interface
SINGLE_TRANSACTION
create
make (s, t: DATA_RESOURCE)
require
source_exists: s /= void
target_exists: t /= void
ensure
source_set: source = s
target_set: target = t
read_mode_set: source.read_mode
write_mode_set: target.write_mode
feature
source: DATA_RESOURCE
target: DATA_RESOURCE
feature
Count: INTEGER is 1
feature
error: BOOLEAN
TRANSACTION
is_correct: BOOLEAN
succeeded: BOOLEAN
feature
reset_error
feature
execute
require TRANSACTION
correct_transaction: is_correct
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- SINGLE_TRANSACTION