A Formal Definition of JML in Coq

and its Application to Runtime Assertion Checking

a Ph.D. Thesis presented by Hermann Lehner

 

     spec    proof comments


Helpers

       43       35        0 EqBoolAux.v

       51       36       25 ListFunctions.v

       45      152       44 ListHelpers.v

        2       12        0 LogicHelpers.v

       34       19       18 OptionHelpers.v

       33       43        0 PosAux.v

       59        0        0 Prelude.v

      124      296        1 Stack.v

       28        7       77 TaggedList.v

       21       21       21 ZHelpers.v


Formalization of JML

      957       18      176 JMLProgram.v

      178        0      105 JMLNotations.v

      120        0       19 JMLExpressionNotations.v

        7        0        2 JMLSyntax.v

       56        0        3 JMLNumeric.v

      566      150       52 JMLDomain.v

      729        0      106 JMLSemantics.v


Operational Semantics

      120       92       35 JMLOpSem.v


Syntactic Desugaring & Implementation

      132        0      207 JMLFull2Basic.v

     1023       26      396 JMLFull2BasicImpl.v

       50        0       27 JMLProgramPlus.v

     1717      259      353 JMLProgramPlusImpl.v


Correctness Proof of RAC

      175      617       12 JMLRac.v

      580     1045       16 JMLRac2.v

      626     2614       17 JMLRac3.v

       78      317       39 JMLRac_1_Correct.v

      115      500       25 JMLRac_2_Correct.v

       80      297       25 JMLRac_3_Correct.v


Total

     7794     6556     1833 total

Browse Formalization