Its CBS illustrates scaling up to a medium-sized language. The start of the specification of OCaml-Light in CBS is at OCaml-Light. The specification is divided into sections corresponding to Chapter 7 of the OCaml Manual.
The OCaml-Light language corresponds closely to the language whose static and dynamic semantics have been specified by Scott Owens in the Ott framework.
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.
- abstract syntax: complete, derived from OCaml Manual
- dynamic semantics: complete
- static semantics: not specified
- disambiguation: incomplete, derived from OCaml Manual
- 177 small programs
- high coverage (to be verified)
Reuse of funcons:
- OCaml Implementation
- OCaml Manual
- A formal specification for OCaml: the Core Language
- Reusable Components of Semantic Specifications
- OCaml, higher-order, functional, imperative, patterns, disambiguation
- recent: Peter Mosses, Neil Sculthorpe
- previous: Martin Churchill, Paolo Torrini
Table of contents