ceph/src/boost/libs/contract/example/meyer97/stack4.e

   1
   2 -- Copyright (C) 2008-2018 Lorenzo Caminiti
   3 -- Distributed under the Boost Software License, Version 1.0 (see accompanying
   4 -- file LICENSE_1_0.txt or a copy at http://www.boost.org/LICENSE_1_0.txt).
   5 -- See: http://www.boost.org/doc/libs/release/libs/contract/doc/html/index.html
   6
   7 //[meyer97_stack4_e
   8 -- Extra spaces, newlines, etc. for visual alignment with this library code.
   9
  10
  11
  12
  13
  14 indexing
  15     destription: "Dispenser with LIFO access policy and a fixed max capacity."
  16 class interface STACK4[G] creation make -- Interface only (no implementation).
  17
  18
  19
  20
  21
  22
  23
  24 invariant
  25     count_non_negative: count >= 0
  26     count_bounded: count <= capacity
  27     empty_if_no_elements: empty = (count = 0)
  28
  29
  30
  31 feature -- Initialization
  32
  33     -- Allocate stack for a maximum of n elements.
  34     make(n: INTEGER) is
  35         require
  36             non_negative_capacity: n >= 0
  37         ensure
  38             capacity_set: capacity = n
  39         end
  40
  41
  42
  43
  44
  45
  46
  47
  48
  49
  50
  51
  52
  53
  54
  55
  56
  57
  58
  59
  60
  61
  62
  63
  64
  65
  66
  67
  68
  69
  70
  71
  72
  73
  74
  75
  76
  77
  78
  79
  80
  81
  82
  83
  84
  85
  86
  87
  88
  89
  90
  91 feature -- Access
  92
  93     -- Max number of stack elements.
  94     capacity: INTEGER
  95
  96
  97
  98
  99
 100     -- Number of stack elements.
 101     count: INTEGER
 102
 103
 104
 105
 106
 107     -- Top element.
 108     item: G is
 109         require
 110             not_empty: not empty -- i.e., count > 0
 111         end
 112
 113
 114
 115
 116
 117
 118 feature -- Status report
 119
 120     -- Is stack empty?
 121     empty: BOOLEAN is
 122         ensure
 123             empty_definition: result = (count = 0)
 124         end
 125
 126
 127
 128
 129
 130
 131
 132
 133     -- Is stack full?
 134     full: BOOLEAN is
 135         ensure
 136             full_definition: result = (count = capacity)
 137         end
 138
 139
 140
 141
 142
 143
 144
 145
 146 feature -- Element change
 147
 148     -- Add x on top.
 149     put(x: G) is
 150         require
 151             not_full: not full
 152         ensure
 153             not_empty: not empty
 154             added_to_top: item = x
 155             one_more_item: count = old count + 1
 156         end
 157
 158
 159
 160
 161
 162
 163
 164
 165     -- Remove top element.
 166     remove is
 167         require
 168             not_empty: not empty -- i.e., count > 0
 169         ensure
 170             not_full: not full
 171             one_fewer_item: count = old count - 1
 172
 173         end
 174
 175
 176
 177
 178
 179
 180
 181
 182
 183
 184
 185
 186
 187
 188
 189
 190
 191
 192
 193
 194
 195
 196
 197 end -- class interface STACK4
 198
 199 -- End.
 200 //]
 201