View Source API Reference corsa v0.1.2
Modules
Assertions in programming are statements that check conditions. They help catch errors early and improve code reliability and maintainability. In Corsa, assertions can work in two ways: by throwing exceptions or logging errors.
Declare allows you to define variable contracts. In Corsa, these contracts restrict the values that may be assigned to a variable.
The decreases contract specifies a function, that when applied to the arguments of the called function, calculates a measure (e.g., an integer). Corsa checks that measure when a function is invoked is strictly greater than the measure in recursive calls.
The expect specifies the acceptable messages in a receive statement.
Postconditions are specifications which must be fulfilled after the execution of a function, thereby certifying that the anticipated output criteria have been satisfied. In Corsa, postconditions are evaluated at runtime. If a postcondition is not satisfied, either an exception or a log is generated.
Preconditions are requirements that must be met before executing a function. It ensures correct behavior and avoids potential errors by specifying conditions for input parameters. In Corsa, preconditions are checked during runtime. If a precondition is not met, an exception or a log is thrown.
SpecArgs contract, also known as type requirements, must be met before executing a function. In Corsa, they are checked during runtime and just prior to the annotated function's execution.
TODO
The init annotation is used to establish the initial state of the state machine.
This module generates a state machine model using contract information.
Macros in this module generate the necessary intrumentation to monitor an Elixir process.
The next annotation is utilized to delineate the transition function of the state machine.
Postconditions are essential conditions that must be fulfilled following the execution of a function, thereby assuring that the anticipated output conditions have been met. In Corsa, postconditions are evaluated during runtime. If a postcondition isn't guaranteed, an exception or log is generated. Within the definition of a state machine, postconditions are able to access the state.
throws verifies if a thrown exception is anticipated. When a state machine is utilized, the
contract has the ability to access the state.
Throws checks if the exception thrown by the annotated function is expected.
Within contracts, there are time bounds to function executions. In Corsa, when an annotated function does not execute within the time bound specified by the contract, a runtime error is thrown.