class SIMPLE_BACKGROUND_JOB

Features exported to INTERNALS_HANDLER

Describe job to be executed in the background, when there nothing more important to do. Such job is ready to run at any time.

Direct parents

conformant parents

BACKGROUND_JOB

Summary

creation features

exported features

Details

set_work (t: FUNCTION [O_ -> TUPLE, R_][TUPLEBOOLEAN], tr: PROCEDURE [O_ -> TUPLE][TUPLE], prio: INTEGER)

t has to return True while continue

require

  • t /= Void

ensure

    set_work (t: FUNCTION [O_ -> TUPLE, R_][TUPLEBOOLEAN], tr: PROCEDURE [O_ -> TUPLE][TUPLE], prio: INTEGER)

    t has to return True while continue

    require

    • t /= Void

    ensure

      Class invariant