+
Point of view
All features
class MOCK_MATCHERS
Summary
Direct parents
Insert list: ANY
Class invariant
Overview
count: INTEGER_32
effective function
valid_index (i: INTEGER_32): BOOLEAN
effective function
effective function
require
out_in_tagged_out_memory
effective procedure
Append terse printable representation of current object in tagged_out_memory.
require
  • locked: tagged_out_locked
ensure
  • still_locked: tagged_out_locked
  • not_cleared: tagged_out_memory.count >= old tagged_out_memory.count
  • append_only: old tagged_out_memory.twin.is_equal(tagged_out_memory.substring(1, old tagged_out_memory.count))
make0
effective procedure
{}
make1 (a1: MOCK_MATCHER)
effective procedure
{}
require
  • a1 /= Void
make2 (a1: MOCK_MATCHER, a2: MOCK_MATCHER)
effective procedure
{}
require
  • a1 /= Void
  • a2 /= Void
make3 (a1: MOCK_MATCHER, a2: MOCK_MATCHER, a3: MOCK_MATCHER)
effective procedure
{}
require
  • a1 /= Void
  • a2 /= Void
  • a3 /= Void
effective procedure
{}
require
  • a1 /= Void
  • a2 /= Void
  • a3 /= Void
  • a4 /= Void
effective procedure
{}
require
  • a1 /= Void
  • a2 /= Void
  • a3 /= Void
  • a4 /= Void
  • a5 /= Void
effective procedure
{}
require
  • a1 /= Void
  • a2 /= Void
  • a3 /= Void
  • a4 /= Void
  • a5 /= Void
  • a6 /= Void
effective procedure
{}
require
  • a1 /= Void
  • a2 /= Void
  • a3 /= Void
  • a4 /= Void
  • a5 /= Void
  • a6 /= Void
  • a7 /= Void
effective procedure
{}
require
  • a1 /= Void
  • a2 /= Void
  • a3 /= Void
  • a4 /= Void
  • a5 /= Void
  • a6 /= Void
  • a7 /= Void
  • a8 /= Void
effective procedure
{}
require
  • a1 /= Void
  • a2 /= Void
  • a3 /= Void
  • a4 /= Void
  • a5 /= Void
  • a6 /= Void
  • a7 /= Void
  • a8 /= Void
  • a9 /= Void
effective procedure
{}
require
  • a1 /= Void
  • a2 /= Void
  • a3 /= Void
  • a4 /= Void
  • a5 /= Void
  • a6 /= Void
  • a7 /= Void
  • a8 /= Void
  • a9 /= Void
  • a10 /= Void
writable attribute
{}
_inline_agent51 (m: MOCK_MATCHER): BOOLEAN
frozen
effective function
{}