This collection of files contains the Netsem specification as of August 2005.

Copyright (c)2005 The Netsem Team: 

  Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell,
  Michael Smith, Keith Wansbrough

This is the PUBLIC VERSION.  Please distribute at will, subject to the
copyright and license given in the file LICENSE-spec-public.

See <http://www.cl.cam.ac.uk/~pes20/Netsem/> for further details.


Contents:

  README-spec-public        - this file
  LICENSE-spec-public       - the copyright license
  VERSIONS-spec-public      - cvs version data for the spec files

Specification
~~~~~~~~~~~~~

- spec support:

  Net_Hol_reln.sig - turn <== to ==> and do Hol_reln (defines the spec constructor)
  Net_Hol_reln.sml - turn <== to ==> and do Hol_reln (defines the spec constructor)

  Version.sig - version tracking constructs - used in spec but not essential
  Version.sml - version tracking constructs - used in spec but not essential

- phasing spec support: 

  Phase.sig - phase control constructs - used in spec, but for symeval purposes only
  Phase.sml - phase control constructs - used in spec, but for symeval purposes only

- spec proper:

  TCP1_LIBinterfaceScript.sml - system calls
  TCP1_auxFnsScript.sml - auxiliary functions
  TCP1_baseTypesScript.sml - base types and typing
  TCP1_errorsScript.sml - error codes
  TCP1_evalSupportScript.sml - typical initial hosts
  TCP1_host0Script.sml - host labels and rule categories
  TCP1_hostLTSScript.sml - host labelled transition system and some auxiliary defs
  TCP1_hostTypesScript.sml - host datatypes
  TCP1_netTypesScript.sml - network datatypes, and .is1/.is2 hack
  TCP1_paramsScript.sml - host behavioural constants
  TCP1_ruleidsScript.sml - rule names
  TCP1_signalsScript.sml - signal names
  TCP1_timersScript.sml - timers
  TCP1_utilsScript.sml - basic syntax and helper functions



--Peter Sewell, for the Netsem team, 2005-08-20.

