new stacks). To describe such algorithms, one usually includes in the ADT definition a create() operation that yields an instance of the ADT, usually with axioms equivalent to the result of create() is distinct from any instance already in use by the algorithm. This axiom may be strengthened to exclude also partial aliasing with other instances. For practical use, such as axiom may still allow implementations of create() to yield a previously created instance that has become inaccessible to the program; however, defining that such an instance even is "the same" is difficult, especially in the abstract (though even a re-used block of memory is only "the same object" in certain senses). Example: abstract stack (imperative) As another example, an imperative-style definition of an abstract stack could specify that the state of a stack S can be modified only by the operations push(S, x), where x is some value of unspecified nature; pop(S), that yields a value as a result, with the constraint that For any value x and any abstract variable V, the sequence of operations { push(S, x); V ← pop(S) } is equivalent to V ← x. Since the assignment V ← x, by definition, cannot change the state of S, this condition implies that V ← pop(S) restores S to the state it had before the push(S, x). From this condition and from the properties of abstract variables, it follows, for example, that the sequence { push(S, x); push(S, y); U ← pop(S); push(S, z); V ← pop(S); W ← pop(S) } where x, y, and z are any values, and U, V, W are pairwise distinct variables, is equivalent to { U ← y; V ← z; W ← x } Here it is implicitly assumed that operations on a stack instance do not modify the state of any other ADT instance, including other stacks; that is, For any values x, y, and any distinct stacks S and T, the sequence { push(S, x); push(T, y) } is equivalent to { push(T, y); push(S, x) }. An abstract stack definition usually includes also a Boolean-valued function empty(S) and a create() operation that returns a stack instance, with axioms equivalent to create() ≠ S for any prior stack S (a newly created stack is distinct from all previous stacks); empty(create()) (a newly created stack is empty); not empty(push(S, x)) (pushing something into a stack makes it