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 14indexing 15 destription: "Dispenser with LIFO access policy and a fixed max capacity." 16class interface STACK4[G] creation make -- Interface only (no implementation). 17 18 19 20 21 22 23 24invariant 25 count_non_negative: count >= 0 26 count_bounded: count <= capacity 27 empty_if_no_elements: empty = (count = 0) 28 29 30 31feature -- 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 91feature -- 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 118feature -- 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 146feature -- 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 197end -- class interface STACK4 198 199-- End. 200//] 201 202