.e

class
    MARBLES

creation {PLAYER}
    make

feature {NONE}
    make
        do
            count := 100
        end

feature {ANY}
    count: INTEGER

feature {PLAYER}
    lose(n: INTEGER)
        require
            enough_count: n <= count
        do
            count := count - n
        end

    win(n: INTEGER)
        do
            count := count + n 
        end

invariant
    positive_count: count >= 0

end