Library JMLProgramPlus
This file is part of
A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking
Ph.D. Thesis by Hermann Lehner
Online available at jmlcoq.info
Authors:
- Hermann Lehner
- David Pichardie (Bicolano)
- Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)
PROGRAM_PLUS extends the PROGRAM signature (JMLProgram)
with full syntax constructs that need explicit representation
and cannot be rewritten in place.
Currently, the added constructs are those for the
representation of method specification cases.
Declare and export the original PROGRAM signature, s.t. PROGRAM_PLUS implementors also fulfill the PROGRAM signature.
Declare Module Program : PROGRAM.
Export Program.
Module METHODSPEC_PLUS.
Import Program.METHODSPEC.
Export Program.
Module METHODSPEC_PLUS.
Import Program.METHODSPEC.
The different kind of method specification cases
Inductive SpecCaseType : Set :=
| lightweight
| behaviour
| normal_behaviour
| exceptional_behaviour.
| lightweight
| behaviour
| normal_behaviour
| exceptional_behaviour.
Special type for the predicate argument of a requires clause,
that can be either a specified expression, \not_specified or \same.
Inductive optionalSame (A : Type) : Type :=
| NotSpecifiedOS : optionalSame A
| SpecifiedOS : A -> optionalSame A
| same : optionalSame A.
| NotSpecifiedOS : optionalSame A
| SpecifiedOS : A -> optionalSame A
| same : optionalSame A.
Full syntax type for a spec header.
@see JML RM 9.4 spec header
Full syntax type for simple body clauses. @see JML RM 9.4 simple-spec-body
Inductive MethodSpecClause : Type :=
| ensuresC (redundant : bool) (pred : optional Expression)
| signalsC (redundant : bool) (pair : Param * optional Expression)
| signalsOnlyC (redundant : bool) (types : list StaticType)
| divergesC (redundant : bool) (pred : optional Expression)
| whenC (redundant : bool) (pred : optional Expression)
| assignableC (redundant : bool) (storeRefs : optional StoreRefList)
| accessibleC (redundant : bool) (storeRefs : optional StoreRefList)
| callableC (redundant : bool) (storeRefs : optional CallableList)
| measuredByC (redundant : bool) (pair : optional Expression * option Expression)
| capturesC (redundant : bool) (storeRefs : optional StoreRefList)
| workingSpaceC (redundant : bool) (pair : optional Expression * option Expression)
| durationC (redundant : bool) (pair : optional Expression * option Expression).
| ensuresC (redundant : bool) (pred : optional Expression)
| signalsC (redundant : bool) (pair : Param * optional Expression)
| signalsOnlyC (redundant : bool) (types : list StaticType)
| divergesC (redundant : bool) (pred : optional Expression)
| whenC (redundant : bool) (pred : optional Expression)
| assignableC (redundant : bool) (storeRefs : optional StoreRefList)
| accessibleC (redundant : bool) (storeRefs : optional StoreRefList)
| callableC (redundant : bool) (storeRefs : optional CallableList)
| measuredByC (redundant : bool) (pair : optional Expression * option Expression)
| capturesC (redundant : bool) (storeRefs : optional StoreRefList)
| workingSpaceC (redundant : bool) (pair : optional Expression * option Expression)
| durationC (redundant : bool) (pair : optional Expression * option Expression).
Full syntax ADT for a generic-spec-case @see JML RM 9.4 generic-spec-case
Module Type GENERIC_SPEC_CASE_TYPE.
Parameter t : Type.
Parameter forallVarDecl : t -> list FORALL_VAR_DECL.t.
Parameter oldVarDecl : t -> list OLD_VAR_DECL.t.
Parameter specHeader : t -> list SpecHeader.
Parameter genericBody : t -> (list MethodSpecClause) + (list t).
End GENERIC_SPEC_CASE_TYPE.
Declare Module GENERIC_SPEC_CASE : GENERIC_SPEC_CASE_TYPE.
Parameter t : Type.
Parameter forallVarDecl : t -> list FORALL_VAR_DECL.t.
Parameter oldVarDecl : t -> list OLD_VAR_DECL.t.
Parameter specHeader : t -> list SpecHeader.
Parameter genericBody : t -> (list MethodSpecClause) + (list t).
End GENERIC_SPEC_CASE_TYPE.
Declare Module GENERIC_SPEC_CASE : GENERIC_SPEC_CASE_TYPE.
Full syntax ADT for a full specification case, i.e. a lightweight-spec-case (JML RM 9.4) or a heavyweight-spec-case (JML RM 9.5) @see JML RM 9.4/9.5
Module Type FULL_SPEC_CASE_TYPE.
Parameter t : Type.
Parameter specCaseType : t -> SpecCaseType.
Parameter visibility : t -> option Visibility.
Parameter isRedundant : t -> bool.
Parameter isCodeContract : t -> bool.
Parameter genericSpecCase : t -> GENERIC_SPEC_CASE.t.
End FULL_SPEC_CASE_TYPE.
Declare Module FULL_SPEC_CASE : FULL_SPEC_CASE_TYPE.
End METHODSPEC_PLUS.
End PROGRAM_PLUS.
Parameter t : Type.
Parameter specCaseType : t -> SpecCaseType.
Parameter visibility : t -> option Visibility.
Parameter isRedundant : t -> bool.
Parameter isCodeContract : t -> bool.
Parameter genericSpecCase : t -> GENERIC_SPEC_CASE.t.
End FULL_SPEC_CASE_TYPE.
Declare Module FULL_SPEC_CASE : FULL_SPEC_CASE_TYPE.
End METHODSPEC_PLUS.
End PROGRAM_PLUS.