Abstract
We extend Jinja to include static fields, methods, and instructions,
and dynamic class initialization, based on the Java SE 8
specification. This includes extension of definitions and proofs. This
work is partially described in Mansky and Gunter's paper at CPP
2019 and Mansky's doctoral thesis (UIUC, 2020).
BSD LicenseDepends On
Used by
Topics
Related Entries
Theories
- Auxiliary
- Type
- Decl
- TypeRel
- Value
- Objects
- Exceptions
- Expr
- WellType
- WellTypeRT
- State
- SystemClasses
- WellForm
- WWellForm
- BigStep
- DefAss
- Conform
- SmallStep
- EConform
- Progress
- JWellForm
- TypeSafe
- Equivalence
- Annotate
- JVMState
- JVMInstructions
- JVMExceptions
- JVMExecInstr
- JVMExec
- JVMDefensive
- SemiType
- JVM_SemiType
- Effect
- EffectMono
- BVSpec
- TF_JVM
- BVExec
- LBVJVM
- BVConform
- ClassAdd
- StartProg
- BVSpecTypeSafe
- BVNoTypeError
- J1
- J1WellForm
- PCompiler
- Hidden
- Compiler1
- Correctness1
- Compiler2
- Correctness2
- Compiler
- TypeComp
- JinjaDCI