new_command: Describe a command for a stateful protocol
In s7contract: Behavioral Contracts and Generative Laws for 'S7'

new_command

R Documentation

Describe a command for a stateful protocol

Description

Commands separate the implementation's effects from a reference model. generate(state) returns an input generator, or NULL when the command is unavailable. execute(fixture, input) calls the implementation. require(state, input) checks the symbolic precondition, and ensure(state, input, output) checks the observed result against the model before the command. Both predicates return one non-missing logical value.

Usage

new_command(
  name,
  generate,
  execute,
  ensure,
  update = function(state, input, output) state,
  require = function(state, input) TRUE
)

Arguments

`name`	Non-empty command name, unique within a command set.
`generate`	Function of the model state returning a generator or `NULL`.
`execute`	Function of the fixture and resolved input returning an output.
`ensure`	Function of the previous state, resolved input, and output returning whether the postcondition holds.
`update`	Function of the previous state, input, and output returning the next state. Defaults to leaving the model unchanged.
`require`	Function of the symbolic state and input returning whether the command is permitted. Defaults to `TRUE`.

Details

update(state, input, output) returns the next model. During generation and shrinking, output is an opaque reference to this command's future result. During execution it is the actual result. Updates may store and pass outputs but must not inspect or compute with them. Expected values should come from the model and inputs, independently of the implementation.

References may be passed as inputs directly or inside ordinary, unclassed lists. They are resolved before execution, including references to NULL outputs. References embedded in other objects are not traversed. Model values must have value semantics: callbacks must not mutate shared environments or other reference objects in the model. Generation, preconditions, and updates must be pure apart from generator draws; preconditions and updates must not draw random numbers.