diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
index 1e1d092510f..b2b973b23e9 100644
--- a/jbmc/src/java_bytecode/java_types.h
+++ b/jbmc/src/java_bytecode/java_types.h
@@ -99,6 +99,102 @@ inline bool can_cast_type<annotated_typet>(const typet &)
   return true;
 }
 
+class java_method_typet : public code_typet
+{
+public:
+  using code_typet::parameterst;
+  using code_typet::parametert;
+
+  /// Constructs a new code type, i.e. method type
+  /// \param _parameters: the vector of method parameters
+  /// \param _return_type: the return type
+  java_method_typet(parameterst &&_parameters, typet &&_return_type)
+    : code_typet(std::move(_parameters), std::move(_return_type))
+  {
+    set(ID_C_java_method_type, true);
+  }
+
+  /// Constructs a new code type, i.e. method type
+  /// \param _parameters: the vector of method parameters
+  /// \param _return_type: the return type
+  java_method_typet(parameterst &&_parameters, const typet &_return_type)
+    : code_typet(std::move(_parameters), _return_type)
+  {
+    set(ID_C_java_method_type, true);
+  }
+
+  const std::vector<irep_idt> throws_exceptions() const
+  {
+    std::vector<irep_idt> exceptions;
+    for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
+      exceptions.push_back(e.id());
+    return exceptions;
+  }
+
+  void add_throws_exceptions(irep_idt exception)
+  {
+    add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
+  }
+
+  bool get_is_final() const
+  {
+    return get_bool(ID_final);
+  }
+
+  void set_is_final(bool is_final)
+  {
+    set(ID_final, is_final);
+  }
+
+  bool get_native() const
+  {
+    return get_bool(ID_is_native_method);
+  }
+
+  void set_native(bool is_native)
+  {
+    set(ID_is_native_method, is_native);
+  }
+
+  bool get_is_varargs() const
+  {
+    return get_bool(ID_is_varargs_method);
+  }
+
+  void set_is_varargs(bool is_varargs)
+  {
+    set(ID_is_varargs_method, is_varargs);
+  }
+
+  bool is_synthetic() const
+  {
+    return get_bool(ID_synthetic);
+  }
+
+  void set_is_synthetic(bool is_synthetic)
+  {
+    set(ID_synthetic, is_synthetic);
+  }
+};
+
+template <>
+inline bool can_cast_type<java_method_typet>(const typet &type)
+{
+  return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
+}
+
+inline const java_method_typet &to_java_method_type(const typet &type)
+{
+  PRECONDITION(can_cast_type<java_method_typet>(type));
+  return static_cast<const java_method_typet &>(type);
+}
+
+inline java_method_typet &to_java_method_type(typet &type)
+{
+  PRECONDITION(can_cast_type<java_method_typet>(type));
+  return static_cast<java_method_typet &>(type);
+}
+
 class java_class_typet:public class_typet
 {
 public:
@@ -112,13 +208,65 @@ class java_class_typet:public class_typet
     {
     }
 
-    /// is a method or field 'final'?
+    /// is a field 'final'?
+    bool get_is_final() const
+    {
+      return get_bool(ID_final);
+    }
+
+    /// is a field 'final'?
+    void set_is_final(const bool is_final)
+    {
+      set(ID_final, is_final);
+    }
+  };
+
+  using componentst = std::vector<componentt>;
+
+  const componentst &components() const
+  {
+    return (const componentst &)(find(ID_components).get_sub());
+  }
+
+  componentst &components()
+  {
+    return (componentst &)(add(ID_components).get_sub());
+  }
+
+  const componentt &get_component(const irep_idt &component_name) const
+  {
+    return static_cast<const componentt &>(
+      class_typet::get_component(component_name));
+  }
+
+  class methodt : public class_typet::methodt
+  {
+  public:
+    methodt() = delete;
+
+    methodt(const irep_idt &_name, java_method_typet _type)
+      : class_typet::methodt(_name, std::move(_type))
+    {
+    }
+
+    const java_method_typet &type() const
+    {
+      return static_cast<const java_method_typet &>(
+        class_typet::methodt::type());
+    }
+
+    java_method_typet &type()
+    {
+      return static_cast<java_method_typet &>(class_typet::methodt::type());
+    }
+
+    /// is a method 'final'?
     bool get_is_final() const
     {
       return get_bool(ID_final);
     }
 
-    /// is a method or field 'final'?
+    /// is a method 'final'?
     void set_is_final(const bool is_final)
     {
       set(ID_final, is_final);
@@ -137,22 +285,16 @@ class java_class_typet:public class_typet
     }
   };
 
-  using componentst = std::vector<componentt>;
+  using methodst = std::vector<methodt>;
 
-  const componentst &components() const
+  const methodst &methods() const
   {
-    return (const componentst &)(find(ID_components).get_sub());
+    return (const methodst &)(find(ID_methods).get_sub());
   }
 
-  componentst &components()
+  methodst &methods()
   {
-    return (componentst &)(add(ID_components).get_sub());
-  }
-
-  const componentt &get_component(const irep_idt &component_name) const
-  {
-    return static_cast<const componentt &>(
-      class_typet::get_component(component_name));
+    return (methodst &)(add(ID_methods).get_sub());
   }
 
   using static_membert = componentt;
@@ -352,102 +494,6 @@ inline bool can_cast_type<java_class_typet>(const typet &type)
   return can_cast_type<class_typet>(type);
 }
 
-class java_method_typet : public code_typet
-{
-public:
-  using code_typet::parameterst;
-  using code_typet::parametert;
-
-  /// Constructs a new code type, i.e. method type
-  /// \param _parameters: the vector of method parameters
-  /// \param _return_type: the return type
-  java_method_typet(parameterst &&_parameters, typet &&_return_type)
-    : code_typet(std::move(_parameters), std::move(_return_type))
-  {
-    set(ID_C_java_method_type, true);
-  }
-
-  /// Constructs a new code type, i.e. method type
-  /// \param _parameters: the vector of method parameters
-  /// \param _return_type: the return type
-  java_method_typet(parameterst &&_parameters, const typet &_return_type)
-    : code_typet(std::move(_parameters), _return_type)
-  {
-    set(ID_C_java_method_type, true);
-  }
-
-  const std::vector<irep_idt> throws_exceptions() const
-  {
-    std::vector<irep_idt> exceptions;
-    for(const auto &e : find(ID_exceptions_thrown_list).get_sub())
-      exceptions.push_back(e.id());
-    return exceptions;
-  }
-
-  void add_throws_exceptions(irep_idt exception)
-  {
-    add(ID_exceptions_thrown_list).get_sub().push_back(irept(exception));
-  }
-
-  bool get_is_final() const
-  {
-    return get_bool(ID_final);
-  }
-
-  void set_is_final(bool is_final)
-  {
-    set(ID_final, is_final);
-  }
-
-  bool get_native() const
-  {
-    return get_bool(ID_is_native_method);
-  }
-
-  void set_native(bool is_native)
-  {
-    set(ID_is_native_method, is_native);
-  }
-
-  bool get_is_varargs() const
-  {
-    return get_bool(ID_is_varargs_method);
-  }
-
-  void set_is_varargs(bool is_varargs)
-  {
-    set(ID_is_varargs_method, is_varargs);
-  }
-
-  bool is_synthetic() const
-  {
-    return get_bool(ID_synthetic);
-  }
-
-  void set_is_synthetic(bool is_synthetic)
-  {
-    set(ID_synthetic, is_synthetic);
-  }
-};
-
-template <>
-inline bool can_cast_type<java_method_typet>(const typet &type)
-{
-  return type.id() == ID_code && type.get_bool(ID_C_java_method_type);
-}
-
-inline const java_method_typet &to_java_method_type(const typet &type)
-{
-  PRECONDITION(can_cast_type<java_method_typet>(type));
-  return static_cast<const java_method_typet &>(type);
-}
-
-inline java_method_typet &to_java_method_type(typet &type)
-{
-  PRECONDITION(can_cast_type<java_method_typet>(type));
-  return static_cast<java_method_typet &>(type);
-}
-
 /// This is a specialization of reference_typet.
 /// The subtype is guaranteed to be a struct_tag_typet.
 class java_reference_typet : public reference_typet