  We present a Coq formalisation of the small-step operational semantics of
Jafun, a small Java-like language with classes. This format of semantics makes
it possible to naturally specify and prove invariants that should hold at each
computation step. In contrast to the Featherweight Java approach the semantics
explicitly manipulates frame stack of method calls. Thanks to that one can
express properties of computation that depend on execution of particular
methods.
  On the basis of the semantics, we developed a type system that makes it
possible to delineate a notion of a compound value and classify certain methods
as extensional functions operating on them. In our formalisation we make a
mechanised proof that the operational semantics for the untyped version of the
semantics agrees with the one for the typed one. We discuss different methods
to make such formalisation effort and provide experiments that substantiate it.
