The built-in compiler generates probabilistic automatons for various model checkers, given a specification in a subset of the Java language. The subset is:

• chosen in order to balance expressivity and simplicity, assuming that the input models are of a moderate algorithmical complexity;
• completed with tags in comments, that are hc–specific extensions, but do not make the language incompatible with standard Java compilers.

Hc aims at the model specification being readable and scalable. These qualities may reduce bugs, and in effect make the checked property values more reliable.

Features:

• the possibility of having a common source for the production implementation and for the model;
• a support for several model checkers, including Prism.
• both the plain Java virtual machine and the Java PathFinder can straightforwardly run the model;
• hooks for analysis, how the model behaves on the JVM – can be used by e. g. custom optimisers;
• ranges on variables, methods and expressions enable testing of self–consistency of the model, also helps checker engines;
• probability and non–determinism;
• a support for clocks;
• thread synchronisation using either simple conditional barriers or semaphores; the latter with a standard set of features, like synchronised blocks;
• players and coalitions for modelling multi–agent systems;
• a special thread interpreted within hc for a convenient definition of the initial state, by e.g. creating and connecting components of the model; it can also be used for the generation of properties to check;
• the built–in interpreter, by doing the initial computation, makes more things known to Hc's optimiser, what in turn may substantially reduce the strain exerted later on a model checker;
• schedulers – as the automatons are not specified directly, they can be generated by applying a set of timing rules to the model defined.

The compiler's library adds features like barrier synchronisation, or simplifies the definition of certain types of models. The library, in the variant for a Java virtual machine, defines counterparts that, depending on their purpose, perform the same action, are invisible or user–definable.