Spec# is an extension of C#. It extends the type system to include non-null types and checked exceptions. It provides method contracts in the form of pre- and postconditions as well as object invariants.
The Spec# static program verifier. This component translates Spec# programs into logical verification conditions. Internally it uses an automatic theorem prover that operates on the verification conditions deduced from the Spec# contract.
An interface to the Spec Explorer tool for test generation and model-based testing.
A unique feature of the Spec# programming system is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads and inter-object relationships.
Spec# (also "specsharp" for search engines and the like), is now available for download. The home page gives a list of related publications.
Recent comments
16 weeks 1 day ago
16 weeks 2 days ago
16 weeks 2 days ago
38 weeks 3 days ago
42 weeks 5 days ago
44 weeks 2 days ago
44 weeks 2 days ago
47 weeks 4 hours ago
51 weeks 4 days ago
51 weeks 4 days ago