package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module WhilelibSource

Sourcemodule 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.

Sourcemodule 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.

Sourcemodule 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.

Sourcemodule While_examples : sig ... end

Example while programs