Specification class

Provides static methods that are useful for writing specifications and interacting with the systematic testing engine.

public static class Specification

Public Members

name description
static Assert(…) Checks if the predicate holds, and if not, throws an exception. (4 methods)
static IsEventuallyCompletedSuccessfully(…) Creates a monitor that checks if the specified task eventually completes its execution successfully, and if not, fails with a liveness property violation.
static Monitor<T>(…) Invokes the specified monitor with the given event.
static RegisterMonitor<T>() Registers a new safety or liveness monitor.
static RegisterStateHashingFunction(…) Registers a new state hashing function that contributes to computing a representation of the program state in each scheduling step.

Remarks

See Specifications Overview for more information.

See Also