Eiffel

Bertrand Meyer, http://www.eiffel.com/

class Stack [G]     feature 
    count : INTEGER
    item : G is require not empty do ... end
    empty : BOOLEAN is do .. end
    full  : BOOLEAN is do .. end
    put (x: G) is
       require not full do ...
       ensure not empty
              item = x
              count = old count + 1

Beispiel sinngemäß aus: B. Meyer: Object Oriented Software Construction, Prentice Hall 1997