CBS-beta / Languages-beta
OC-L-Start 
Language "OCaml Light"

Syntax
  START: start ::= unit-implementation
Semantics
  start[[ _:start ]] : =>environments|null-type



Rule
  start[[ UI ]] = 
    initialise-binding initialise-storing initialise-giving
    finalise-failing finalise-throwing
      interpret[[ UI ]]

[
#1  Lexical conventions
#2  Values
#3  Names
#4  Type expressions
#5  Constants
#6  Patterns
#7  Expressions
#8  Type and exception definitions
#9  Classes
#10 Module interfaces
#11 Module implementations
#12 Core library
#A  Disambiguation
]


/*
  The dynamic semantics of the OCaml Light language is specified here in CBS.
  The specification is divided into sections corresponding to Chapter 7 of the
  [OCaml System Manual](https://caml.inria.fr/pub/docs/manual-ocaml-4.06).
  The section numbers listed above are links to the respective files.
  
  The OCaml Light language corresponds closely to the language whose static
  and dynamic semantics have been specified by Scott Owens in the Ott framework
  (https://github.com/ott-lang/ott/tree/master/examples/ocaml_light).
  
  The correctness of the CBS semantics (in relation to the implementation
  provided by the OCaml developers) has been partially tested by generating
  a parser, translator, and interpreter from the specifications, and checking
  that the results of running a suite of about 150 small programs using the
  generated implementation correspond to the results of running them directly.

*/


/* CBS-beta/Languages-beta/OCaml-Light/OC-L-cbs released 2018-07-07

* Status: 
  - abstract syntax:   complete, derived from [OCaml Manual]
  - dynamic semantics: complete
  - static semantics:  not specified
  - disambiguation:    incomplete, derived from [OCaml Manual]
* Tests:
  - 177 small programs
  - high coverage (to be verified)
* Evolution:
  - supersedes [Reusable Components of Semantic Specifications]
* References:
  [OCaml Implementation]: 
    http://ocaml.org/docs/install.html
  [OCaml Manual]:
    https://caml.inria.fr/pub/docs/manual-ocaml-4.06
  [A formal specification for OCaml: the Core Language]:
    https://github.com/ott-lang/ott/tree/master/examples/ocaml_light
  [Reusable Components of Semantic Specifications]:
    http://plancomps.org/taosd2015
* Keywords: 
  - OCaml, higher-order, functional, imperative, patterns, disambiguation
* Main contributors:
  - recent: Peter Mosses, Neil Sculthorpe
  - previous: Martin Churchill, Paolo Torrini


*/