CFEM.C.matrix

CFEM.C.element

CFEM.C.fem

CFEM.C.mesh

CFEM.C.quadrules

CFEM.C.shapes

CFEM.C.spec_matrix

CFEM.C.verif_matrix

CFEM.C.nonexpansive

• Machinery for proving the nonexpansiveness of object-oriented interfaces.

CFEM.C.spec_shapes: VST function specification for shape

• • shape_spec: VST funspec of C shape function

CFEM.C.verif_shapes_base

CFEM.C.verif_shapes1d: VST correctness proofs for 1-dimensional shape functions

CFEM.C.verif_shapes2d: VST correctness proofs for 2-dimensional shape functions

CFEM.C.verif_shapes2dP2: VST correctness proofs for 2dP2 shape function

CFEM.C.VSU_shapes

• CFEM.VSU_shapes: Verified Software Unit for all the C shape functions

CFEM.model

CFEM.matrix_util

CFEM.shape: Lagrange shape functions, and some supporting theory

• • Definition of a package of real-valued shape functions.
  • We enclose the shape record in a module
    • Convex hull of a set of vertices
    • Multivariate Polynomials are continuously differentiable
    • Lemmas needed only until we switch to MathComp-Analysis 1.16
  • A whole bunch of supporting lemmas and proof-automation tactics
• Instances: shape-function-sets of various dimensions and degrees
  • 1dP1: 1-dimension, degree 1
  • 1dP2: 1-dimension, degree 2
  • 1dP3: 1-dimension, degree 3
  • 2dP1: 2-dimensional cuboid, degree 1
  • 2dT1: 2-dimensional simplex, degree 1
  • 2dP2: 2-dimensional cuboid, degree 2, with center vertix
  • 2dS2: 2-dimensional cuboid, degree 2, without center vertix (Serendipity element)

CFEM.shapefloat: floating-point shape functions

• • Bounds
  • FShape
• Instances
  • 1dP1: 1-dimension, degree 1
  • 1dP2: 1-dimension, degree 2
  • 1dP3: 1-dimension, degree 3
  • 2dP1: 2-dimension, degree 1
  • 2dP2: 2-dimension, degree 2, with center point
  • 2dS2: 2-dimension, degree 2, without center point (Serendipity element)
  • 2dT2: 2-dimension triangle, degree 1

CFEM.shape_accuracy: Roundoff-error bounds for shape functions

• The Shape Accuracy Property
  • • bounds_enclose:
    • roundoff_bound_lemma: The accuracy proof of a set of shape functions
  • Utility tactics and lemmas
• Instances: accuracy proofs for all the elements
  • 1dP1: 1-dimensional, degree 1
    • Extracting the floating-point shape functions into "ordinary" floating-point operations
    • Calculating the error bound
    • first shape function
    • second shape function
    • derivative function accuracy bounds
    • 1dP1 main result
  • 1dP2: 1-dimensional, degree 2
    • Extracting the floating-point shape functions into "ordinary" floating-point operations
    • first shape function
    • second shape function
    • third shape function
    • shape derivative functions
    • 1dP2 main result
  • 2dP1: 2-dimensional, degree 1
    • Extracting the floating-point shape functions into "ordinary" floating-point operations
    • four shape functions
    • shape derivative functions
    • 2dP1 main result
    • 2dT1 main result
  • 2dT1: 2-dimensional triangle, degree 1
    • Extracting the floating-point shape functions into "ordinary" floating-point operations
    • three shape functions
    • shape derivative functions
    • 2dT1 main result
  • 2dP2: 2-dimensional, degree 2
  • 2dS2: 2-dimensional, degree 2, Serendipity