• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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-simplified-uml

    ATJ tutorial: About the Simplified UML Class Diagrams.

    This tutorial uses simplified UML class diagrams to illustrate the AIJ Java classes. These simplified UML diagrams are briefly described in this tutorial page. It may be skipped if the reader is already familiary with UML.

    Diagram Notation

    Each class is depicted as a box containing its name. Abstract classes have italicized names. Public classes have names preceded by +, while package-private classes have names preceded by ~.

    Inheritance (`is a') relationships are indicated by lines with hollow triangular tips. Composition (`part of') relationships are indicated by lines with solid rhomboidal tips, annotated with the names of the containing class instances' fields that store the contained class instances, and with the multiplicity of the contained instances for each containing instance (0..* means `zero or more').

    The dashed boxes are just replicas to avoid clutter.

    Simplifications

    These UML class diagrams are simplified because the class boxes do not contain fields and methods, as they should in a full UML class diagram.

    Previous: Relationship with AIJ

    Next: Java Representation of the ACL2 Values