Timing UDP: The HOL Model

Scripts

The HOL Kananaskis-0 scripts for the main definitions and HOL theorems, and the resulting theory signatures:

• TNet_typesScript.sml; TNet_typesTheory.sig
• TNet_auxfnsScript.sml; TNet_auxfnsTheory.sig
• TNet_oksScript.sml; TNet_oksTheory.sig
• TNet_LIBinterfaceScript.sml; TNet_LIBinterfaceTheory.sig
• TNet_host0Script.sml; TNet_host0Theory.sig
• TNet_hostLTSScript.sml; TNet_hostLTSTheory.sig
• TNet_threadAxScript.sml; TNet_threadAxTheory.sig
• TNet_NetworksScript.sml; TNet_NetworksTheory.sig
• TNet_host_theorem1Script.sml; TNet_host_theorem1Theory.sig
• TNet_host_theorem2Script.sml; TNet_host_theorem2Theory.sig

Revision numbers and dates of the above files are listed here.

The host transition semantics

The host transition semantics in TNet_hostLTSScript.sml above has been rendered by our automatic typesetting tools, and can be viewed here as gzipped PostScript.

Return to project page