1. The instructionIsTypeSafe rule for getfield mentions that "FieldClass must not be an array type." This is true by construction, because the rule uses functor 'class' in the validTypeTransition clause. However, the Prolog term 'class(FieldClass)' is ill-formed - 4.10.1.2 introduced 'class' as 2-arity. The rule should add:

  currentClassLoader(Environment, CurrentLoader),

and use class(FieldClass, CurrentLoader) in validTypeTransition.

2. The instructionIsTypeSafe rule for putfield should mention that "FieldClass must not be an array type.", since it uses the functor 'class' (correctly, with two args) in the canPop clause.

3. The getstatic and putstatic instructions don't rely on the declaring class of the field (indicated by the underscore in _FieldClass), so there is no need to modify their rules.