• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
          • Atj
            • Atj-implementation
            • Atj-tutorial
              • Atj-tutorial-deep
              • Atj-tutorial-ACL2-values
              • Atj-tutorial-native-functions
              • Atj-tutorial-deep-guards
              • Atj-tutorial-ACL2-terms
              • Atj-tutorial-evaluator
              • Atj-tutorial-background
              • Atj-tutorial-ACL2-environment
              • Atj-tutorial-translated
              • Atj-tutorial-shallow
              • Atj-tutorial-tests
              • Atj-tutorial-customization
              • Atj-tutorial-motivation
              • Atj-tutorial-deep-shallow
              • Atj-tutorial-screen-output
              • Atj-tutorial-shallow-guards
              • Atj-tutorial-simplified-uml
              • Atj-tutorial-aij
            • Aij
            • Language
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Atj-tutorial

    Atj-tutorial-aij

    ATJ tutorial: Relationship with AIJ.

    This tutorial page clarifies the relationship between ATJ and AIJ.

    Purpose of AIJ

    AIJ is related to, but independent from, ATJ. ATJ generates Java code that needs at least part of AIJ to run: in this sense, ATJ depends on AIJ. Although the development of AIJ has been motivated by ATJ, AIJ does not need or depend on ATJ: it can be used independently. However, AIJ's main use is as support for ATJ.

    More Information on AIJ

    See the AIJ manual page for information about AIJ as a stand-alone entity, independent from ATJ. However, this ATJ tutorial will describe many aspects of AIJ that are necessary or useful to understand and use ATJ.

    Previous: Background on the Evaluation Semantics of ACL2

    Next: About the Simplified UML Class Diagrams