CFEM.alloc

CFEM.assemble

CFEM.bandmat

CFEM.densemat

CFEM.element

CFEM.fem

CFEM.mesh

CFEM.quadrules

CFEM.shapes

CFEM.spec_alloc

CFEM.verif_alloc

CFEM.spec_densemat: VST specifications of functions on dense matrices.

• • Corresponds to C program densemat.h and densemat.c
  • Abstracting the floating-point precision
  • Conversions between floats, float-options, and val
  • Representation predicates for dense matrices
• Function specifications (funspecs)
• Not-yet-specified functions
• Building the "Abstract Specification Interface", the list of funspecs for this module

CFEM.verif_densemat: VST proofs of functions on dense matrices.

• • Corresponds to C program densemat.c
• Prologue.
• VSU definitions
• Many useful supporting lemmas about column_major, ordinal, ord_enum, etc.
• Tactics for ordinals
• densemat_malloc verification
• densemat_free verification
• Unpacking dependently typed WITH components
• densemat_clear verification
• densemat_get verification
• densemat_set verification
• densemat_addto verification
• Tactics for calling matrix subscripting functions
• data_norm and densemat_norm verification
• densemat_cfactor verification: Cholesky factorization
• densemat_csolve verification: Cholesky solve by forward substitution and back substitution
• Packaging the densematVSU, the Verified Software Unit

CFEM.floatlib

CFEM.matrix_model: Functional models of matrix operations

• Prologue: typical imports for MathComp floating-point matrix functional models
• MathComp matrices over a nonring
• Functional model of Cholesky decomposition (jik algorithm)
• Definitions for manipulating triangular matrices