Ex Contract v0.1.2 ExContract.CompileState View Source

This module is not meant to be used directly by client code. This module holds compilation state for ExContract. Stores each condition and optional message in corresponding requires or ensures lists.

Link to this section Summary

Types

t()

Defines fields that store ExContract compile state.

:requires - list of ExContract.ConditionMsg that define a single method pre-conditions.
:ensures - list of ExContract.ConditionMsg that define a single method post-conditions

Functions

add_ensure(state, condition)

Adds ensures condition of type ExContract.ConditionMsg to the ensures list. The condition is associated with nil message

add_ensure(state, condition, msg)

Adds a ensures condition of type ExContract.ConditionMsg to the ensures list. The condition is associated with provided message

add_require(state, condition)

Adds requires condition of type ExContract.ConditionMsg to the requires list. The condition is associated with nil message

add_require(state, condition, msg)

Adds requires condition of type ExContract.ConditionMsg to the requires list. The condition is associated with provided message

new()

Returns an empty state where both :requires and :ensures list are empty

Link to this section Types

t()

t() :: %ExContract.CompileState{
  ensures: [ExContract.ConditionMsg.t()],
  requires: [ExContract.ConditionMsg.t()]
}

Defines fields that store ExContract compile state.

:requires - list of ExContract.ConditionMsg that define a single method pre-conditions.
:ensures - list of ExContract.ConditionMsg that define a single method post-conditions.

Link to this section Functions

add_ensure(state, condition)

add_ensure(state :: ExContract.CompileState.t(), condition :: tuple()) ::
  ExContract.CompileState.t()

Adds ensures condition of type ExContract.ConditionMsg to the ensures list. The condition is associated with nil message.

add_ensure(state, condition, msg)

add_ensure(
  state :: ExContract.CompileState.t(),
  condition :: tuple(),
  msg :: String.t()
) :: ExContract.CompileState.t()

Adds a ensures condition of type ExContract.ConditionMsg to the ensures list. The condition is associated with provided message.

add_require(state, condition)

add_require(state :: ExContract.CompileState.t(), condition :: tuple()) ::
  ExContract.CompileState.t()

Adds requires condition of type ExContract.ConditionMsg to the requires list. The condition is associated with nil message.

add_require(state, condition, msg)

add_require(
  state :: ExContract.CompileState.t(),
  condition :: tuple(),
  msg :: String.t()
) :: ExContract.CompileState.t()

Adds requires condition of type ExContract.ConditionMsg to the requires list. The condition is associated with provided message.

new()

new() :: ExContract.CompileState.t()

Returns an empty state where both :requires and :ensures list are empty.