Provides static methods that are useful for writing specifications and interacting with the systematic testing engine.
public static class Specification
|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.|
See Specifications Overview for more information.
- namespace Microsoft.Coyote.Specifications
- assembly Microsoft.Coyote