Initial release

Initial release of HOL4 formalization of a theory of specifications, components, contracts, and compositionality.

Requirements:

• Poly/ML 5.7.1 (or later)
• HOL4 trindemossen-1

The default Makefile task, which assumes Holmake is available on the system, builds all core HOL4 theories:

make

List of HOL4 files

• folStringScript.sml: first-order logic (FOL) with string identifiers, based on the FOL formalization in HOL4 examples, port from Harrison's HOL Light formalization
• folStringInterpScript.sml: some simple first-order theories using string identifiers, for validation
• compSpecUtilityScript.sml: some utility definitions and results
• compSpecScript.sml: definition of abstract syntax for specifications, components, and predicates, and definition of proof systems
• compSpecMetaScript.sml: semantics and metatheory of specifications and components, including proof system soundness
• compSpecFolScript.sml: interpretation as first-order theory
• compSpecExampleScript.sml: examples of proof system use
• mitlScript.sml: MITL formal semantics
• compSpecMitlScript.sml: instantiation of specifications for MITL
• compSpecMitlFLDScript.sml: instantiation for a fuel level display (FLD) system

Key definitions and results

First-order logic

• The abstract syntax of FOL and satisfaction relation for FOL that uses strings for atomic propositions in folStringScript.sml:
  • Datatype: sterm = ... (line 5)
  • Datatype: sform = ... (line 9)
  • Definition sholds: ... (line 60)
• Equivalence of sholds relation with holds relation that uses numbers for atomic propositions from HOL4 examples in folStringScript.sml:
  • Theorem sholds_holds: ... (line 265)
  • Theorem holds_sholds: ... (line 275)

Specification language syntax and semantics

• The (non-extended) specification language abstract syntax in compSpecScript.sml:
  • Sc = (* specification constant *) ... (line 52)
  • c = (* component term *) ... (line 58)
  • S = (* specification term *) ... (line 72)
  • P = (* component specification predicate *) ... (line 96)
• Proof system for the non-extended specification language as an inductive predicate in compSpecScript.sml:
  • Inductive spec_proof: (* defn spec_holds *) ... (line 451)
• Semantics of the (non-extended) specification language in compSpecMetaScript.sml:
  • Definition c_sem: ... (semantics of components) (line 28)
  • Definition S_sem: ... (semantics of specifications) (line 36)
  • Definition P_sem: ... (semantics of predicates) (line 55)

Specification language metatheory

• Interpretation of the (non-extended) specification language as a FOL theory in compSpecFolScript.sml:
  • Definition spec_interp_func: ... (line 7, interpretation of function symbols and constants)
  • Definition spec_interp_pred: ... (line 24, interpretation of predicates)
  • Definition spec_interp_smodel: ... (line 36, first-order structure/signature)
• Translation of (non-extended) specification language to FOL formulas in compSpecFolScript.sml:
  • Definition c2sterm: ... (line 43)
  • Definition S2sterm: ... (line 51)
  • Definition P2sform: ... (line 67)
  • Definition cSval: ... (line 99)
• Theorem 1: soundness of specification language predicate translation to FOL in compSpecFolScript.sml:
  • Theorem P_sem_sholds: ... (line 172, soundness for satisfaction relation with strings for atomic propositions)
  • Theorem P_sem_holds: ... (line 261, soundness for satisfaction relation with numbers for atomic propositions)
• Theorem 2: proof system soundness w.r.t. specification language semantics in compSpecMetaScript.sml:
  • Definition spec_system_sound: ... (line 101 definition of a sound proof system)
  • Theorem spec_holds_system_sound: ... (line 1562 , soundness for proof system defined in spec_proof inductive predicate)
• Soundness of decomposition of proof of a specification language predicate c1 * c2 * c3 : S0 into proofs of individual components and specification refinement proof in compSpecMetaScript.sml:
  • Theorem compositionality_contracts_three: ... (line 1918)

Specification language and proof system examples

• Example 4: compositional specification and proof example in compSpecExampleScript.sml:
  • Definition example_Ps: ... (line 135, premises)
  • Definition example_goal: ... (line 143, goal)
  • Theorem example_refine_spec_holds: ... (line 413, proof system proof of goal assuming premises)
  • Theorem example_refine_sem_spec_holds: ... (line 577, semantic predicate theorem using soundness of proof system)

Extended specification language syntax and semantics

• Interval and MITL abstract syntax in compSpecScript.sml:
  • I = ... (line 23, interval)
  • f = ... (line 32, MITL formula)
• MITL semantics in mitlScript.sml:
  • Definition interval_sem: ... (line 8, interval semantics)
  • Type timed_word = ... (line 68, timed word definition)
  • Definition mitl_general_sem: ... (line 120, MITL semantics as sets of timed words)
• Extended specification language syntax in compSpecScript.sml:
  • T = (* temporal specification constant *) ... (line 45)
  • St = (* temporal specification term *) ... (line 64)
  • Pt = (* temporal component specification predicate *) ... (line 80)
• Extended specification language proof system as inductive predicate in compSpecScript.sml:
  • Inductive spec_temporal_proof: (* defn spec_temporal_holds *) ... (line 687)
• Semantics of the extended specification language in compSpecMitlScript.sml:
  • Definition St_sem: ... (line 7, semantics of temporal specification terms)
  • Definition Pt_sem: ... (line 29, semantics of temporal predicates)
• Metatheory of extended specification language in compSpecMitlScript.sml:
  • Inductive spec_temporal_mitl_proof: ... (line 82, MITL proof system rule)
  • Definition spec_temporal_mitl_system_sound: ... (line 88, temporal proof system soundness)
  • Theorem spec_temporal_mitl_holds_system_sound: ... (line 101, soundness of MITL proof system rule)

Fuel-level display (FLD) system model

• FLD instantiation in compSpecMitlFLDScript.sml:
  • Type state_FLD = ... (line 16, FLD states as mappings from system variables to values)
  • Definition state_holds_FLD: ... (line 23, constraint expressions relation for FLD states)
  • Type timed_word_FLD = ... (line 61, FLD timed words)
  • Definition omega_FLD: ... (line 63, FLD system runs as set of timed words)
  • Definition spec_temporal_holds_FLD_def: ... (line 85, temporal proof system instantiation for FLD)