Contract Compositionality

A HOL4 formalization of a theory of specifications, components, contracts, and compositionality. The formalization largely follows a paper by Nyberg, Westman, and Gurov. Some parts build on an earlier formalization by Hedengran.

Building

Requirements:

• Poly/ML 5.8.1 (or later)
• HOL4 kananaskis-14

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

make

Files

• folStringScript.sml: first-order logic with string identifiers
• folStringInterpScript.sml: some simple first-order theories using string identifiers
• compSpecUtilityScript.sml: some utility definitions and results
• compSpecScript.sml: definition of abstract syntax for specifications, components, and predicates, and definition of proof system
• compSpecMetaScript.sml: semantics and metatheory of specifications and components, including proof system soundness
• compSpecFolScript.sml: interpretation as first-order theory