Library Common

• Common helper definitions and facts for the project
  • Functions properties.
  • Decidability of equality and other properties.
  • Some additional tactics general enough to be put here.

Library ValuesNTypes

• Values used within JVM and their types
  • Prerequisities
    • Names
    • Program counter
    • Numeric values
      • Imported modules
    • Locations
  • Main definitions
    • JVM values
    • Types
    • Kinds of values
  • Mappings and transformations
    • Kind for value or type
    • Default values
    • Conversions between numeric values
    • Conversion between stack and variable values
      • For actual values
      • For kinds
      • Consistency of mappings defined for values and for kinds
    • Conversion between stack and array values
      • For actual values
      • For kinds
      • Consistency of mappings defined for values and for kinds
  • Size of values

Library Numeric

• Signature
  • Original Bicolano staff
  • Added in CoJaq version
    • Constants
    • Comparison operators (bool).
• Implementation
• Properties

Library FNumeric

Library Char

• Signature
  • Original Bicolano staff
• Implementation

Library ArithOps

Library Arithmetic

• Definition of all arithmetic operations
  • General definitions
  • Specialised arithmetics for particular kinds
    • Reference
    • returnAddress
    • Integer
    • Float
    • Long
    • Double
  • All together

Library ProgramStructures

• Program sructures
  • Included modules
  • Program counters and offsets
  • Variable indices
• Program structures enriched with maps on TPC and TVar
  • PROGRAM_STRUCTURES
  • Maps

Library Program

• Bytecode program
  • Included modules
  • Instructions
    • Frame-level instructions
    • Heap access operations
    • Other operations and ulimate definition of CoJaq instruction
  • Program and its components
    • Methods
    • Fields
    • Classes and inheritance
    • Program
    • Subtype relation
• Program with constructors
  • • Included and required modules
  • PC and offsets
  • Methods
  • Classes and programs

Library Heap

• Heap and objects
  • Included modules
  • Basic elements
  • Monitors
  • Objects stored in heap
    • Ordinary objects
    • Arrays
    • Heap values
  • Heap
  • Specification
• Specification of monolitic heap

Library RuntimeStructures

• JVM runtime structures
  • Included modules
  • Local variables array
    • Local values stack.
  • Concretisation of the generic structures introduced above
  • Projections between actual and "shadow" structures
  • Frame (corresponding to method call)
  • Threads and whole JVMs
  • Result or exception
  • Additional definitions related to runtime structures
    • Helper definitions for lists and operand stacks
    • Local variables initialisation
    • Resut or exception

Library ProgramStructuresImpl

• Implementation of PROGRAM_STRUCTURES
  • Included definitions
  • Names
  • Var
  • Maps

Library RuntimeStructuresImpl

• Implementation of PROGRAM_STRUCTURES
  • Included modules
  • Local variables array
  • Concretisation of generic structures introduced above
  • Projections between actual and "shadow" structures
  • Frame (corresponding to method call)
  • Threads and whole JVMs

Library AllStructures

Library Sem_Stackop

• Semantics of stack instructions
  • Included modules
  • Generic operations
  • Dynamic semantics
  • Static semantics
    • Lower level support for static semantics
    • The actual definition
    • Correctness

Library Sem_Var

• Semantics of local variable operations
  • Included modules
  • Var operation constraints
  • Dynamic semantics
  • Static semantics
    • Correctness

Library Sem_Cond

• Semantics of jump operations
  • Included modules
  • Auxiliary definitions
  • Dynamic semantics
  • Static semantics
    • Lower level support for static semantics
  • Static semantics

Library Sem_Frame

• Semantics of in-frame operations
  • Included modules
  • Auxiliary definitions
  • Dynamic semantics
  • Static semantics
  • In-frame program execution

Library Sem_Monitor

• Semantics of monitor instructions

Library Sem_Heap

• Semantics of heap instructions

Library Sem_Call

• Semantics of call and return
  • Included modules
  • Auxiliary definitions
    • Lookup specified as a semantic rule
  • Dynamic semantics

Library Semantics

• The semantics --- top level definitions
  • Included modules
  • Auxiliary definitions
  • Detailed semantics
    • Semantics of IThrow
  • Thread-level semantics
  • Top-level definition

Library ProgramAssertions

• Program assertions
  • Included modules
  • Frame-level assertions
  • Logic to prove partial correctness
• Creating programs with assertions

Library Instructions

• All JVML instructions represented in CoJaq

Library Program_A

• Program example

Library IAdd

• Example verification of program "2 + 2"
  • Modules used
  • Definitions specific to this example
    • Program
    • States
• 2+2 example -- proofs
  • Auxiliary lemmas and definitions
    • Basic arithmetic properties
    • Consistency of state definition
    • Lemmas related to getting intructions from program
  • State transitions
    • Arithmetic level (binop semantcs)
      • Properties in existential form
      • Properties in general "implication" form
    • StackOp semantics level
      • Properties in existential form
      • Properties in general "implication" form
    • Frame level
      • Properties in existential form
      • Properties in general "implication" form
    • Thread level -- semInsrt
      • Properties in existential form
      • Properties in general "implication" form
    • Thread level -- stepThread
      • Properties in existential form
      • Properties in general "implication" form
    • Whole JVM level -- step
      • Properties in existential form
      • Properties in general "implication" form
    • Transitive closures of main relations

Library Loop

• Loop example
  • Modules used
  • The program and the properties to verify
    • Parameter n
    • Program
    • The initial state
  • Basic lemmas and auxiliary definitions
    • Lemmas related to arithmetics
    • Auxiliary definitions
    • Lemmas and tactics
  • Assertion for each position in program
  • Proofs of single transitions
  • Formulation and proof of the main inductive lemma

Library Loop_Assertions

• Loop example --- "program assertions" version
  • Modules used
  • The program and the properties to verify
    • Parameter n
    • Program
    • The initial state
  • Basic lemmas and auxiliary definitions
    • Lemmas related to arithmetics
    • Auxiliary definitions
    • Lemmas and tactics
  • Assertion for each position in program
  • Proofs of single transitions