• Parameterized Recirsive Type
  • Modified version of Karl Crary's Bar Type Theory
  • Class Signature
  • Class Definition
  • J Type Specification
  • J Signature
  • Classes produced by a J Signature
  • J Environment
  • J Expression
  • J Statement
  • J Hoare Predicate
  • Verification examples