Have a look at the "step" method in the "State" class in the "fsm.kmt" file.

// Go to the next state
operation step(c : String) : String raises FSMException is

// Declaration of the pre-condition
pre notVoidInput is
   c != void and c != ""

do
   // Get the valid transitions
   var validTransitions : Collection<Transition> 
   validTransitions :=	outgoingTransition.select { t | t.input.equals(c) }
   // Check if there is one and only one valid transition
   if validTransitions.empty then raise NoTransition.new end
   if validTransitions.size > 1 then raise NonDeterminism.new end

   // Fire the transition
   result := validTransitions.one.fire
end

// Declaration of the post-condition
post notVoidOutput is
   result != void and result != ""

There is a pre condition which says that the character given as a parameter must not be void or empty string. The post condition says that the result must not be void or empty string. For each "step" method call, the pre and post conditions will be checked. If there are evaluated as false, the program is aborted otherwise the program goes on. Look at the run configuration named "loaderFSM4prepost". Open the file (../models/sample1postv.fsm) used as parameter for this configuration. Observe the finite state diagram.