class CLARG_NOT
Summary
Direct parents
Inherit list: COMMAND_LINE_ARGUMENT
Class invariant
Overview
Creation features
{COMMAND_LINE_ARGUMENT}
Features
{ANY}
{COMMAND_LINE_ARGUMENTS, COMMAND_LINE_ARGUMENT}
{}
{ANY}
is_repeatable: BOOLEAN
is False
constant attribute
{ANY}
True if the argument is repeatable; False if unique.
prefix "not": COMMAND_LINE_ARGUMENT
effective function
{ANY}
(tentative; don't use it, the semantics is not well defined)
ensure
  • Result /= Void
is_set: BOOLEAN
effective function
{ANY}
True if the option is present and correct.
is_mandatory: BOOLEAN
effective function
{ANY}
True if the argument must be present.
is_set_at (context: COMMAND_LINE_CONTEXT): BOOLEAN
effective function
{ANY}
True if the option is present and correct at the given context.
require
  • context.is_parsed
ensure
  • Result implies is_set
  • not is_repeatable implies Result = is_set
prepare_parse
effective procedure
ensure
  • not is_set
parse_command_line (context: COMMAND_LINE_CONTEXT): COMMAND_LINE_CONTEXT
effective function
require
  • context.is_parsed
undo_parse (context: COMMAND_LINE_CONTEXT)
effective procedure
require
  • is_set_at(context)
ensure
  • not is_set_at(context)
  • not is_repeatable implies not is_set
usage_summary (stream: OUTPUT_STREAM)
effective procedure
ensure
  • not detailed
usage_details (stream: OUTPUT_STREAM)
effective procedure
ensure
  • detailed
writable attribute
{}
make (a_arg: COMMAND_LINE_ARGUMENT)
effective procedure
{}
require
  • a_arg /= Void
detailed: BOOLEAN
writable attribute
{}
effective function
{ANY}
Arguments disjunction.
Useful to implement mutually exclusive sets of arguments.
require
  • other /= Void
ensure
  • Result /= Void
infix "or else" (other: COMMAND_LINE_ARGUMENT): COMMAND_LINE_ARGUMENT
effective function
{ANY}
Arguments disjunction.
Useful to implement mutually exclusive sets of arguments.
require
  • other /= Void
ensure
  • Result /= Void
effective function
{ANY}
Arguments conjunction.
All the arguments are checked, in any order.
require
  • other /= Void
ensure
  • Result /= Void
infix "and then" (other: COMMAND_LINE_ARGUMENT): COMMAND_LINE_ARGUMENT
effective function
{ANY}
Arguments conjunction.
All the arguments are checked, in any order.
require
  • other /= Void
ensure
  • Result /= Void