indexing
      status: "See notice at end of class"
      date: "$Date$"
      revision: "$Revision$"
      access: execute, immediate, prepare
      product: eiffelstore
      database: all_bases
class interface
      DB_EXEC
create 
      make
                  
            ensure
                  execution_status: not immediate_execution
feature 
      immediate_execution: BOOLEAN
                  
      is_tracing: BOOLEAN
                  
      trace_output: FILE
                  
            ensure
                  destination_file_present: Result = io.error
      
feature 
      set_immediate
                  immediate_executiontrue
                  
                  
            ensure
                  execution_status: immediate_execution
      set_trace
                  
            ensure
                  trace_status: is_tracing
      unset_immediate
                  immediate_executionfalse
                  
                  PREPAREEXECUTE
            ensure
                  execution_status: not immediate_execution
      unset_trace
                  
            ensure
                  trace_status: not is_tracing
      
invariant
             ANY
      reflexive_equality: standard_is_equal (Current)
      reflexive_conformance: conforms_to (Current)
end -- DB_EXEC