function Push(item)
[
//Limit to 10 items
 pre(me.Count < 10 ); 
 post();
 invariant();
]
{
 //me is mutated object, 
 //stack in this case
 me.Push(item);
}

function Pop()
[//Check emptiness
 pre(me.Count > 0);
 post();
 invariant();
]
{
 return me.Pop();
}

stack = new Stack<|int|>();

//Create Mutant
//1. Set Functions, override stack.Push
mObject=[Push->Push,PopCheck->Pop];
//2. Capture object
mObject.Mutate(stack);

for (i=0; i<5; i++)
  mObject.Push(i);

Console.WriteLine((string)mObject.PopCheck());