Module Whilelib

module Analysis_sva : sig ... end

This module presents the implementation of a simple example analyzer for the while language. It is detailed in the While tutorial's chapter3.

module Cinterpreter : sig ... end

Given the while syntax presented in While_ast, in this module Cinterpreter provides the concrete interpreter for the AST containing expressions and commands. Towards this goal, we utlize Var module to refer to named storage locations and then define each concrete state using State as a map from each Var.t to an integer Z.t.

module While_analysis : sig ... end

This module presents the implementation of a simple example analyzer for the while language using codex constructs. It is detailed in the While tutorial's chapter4.

module While_examples : sig ... end

Example while programs