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
27 weeks 1 day ago
27 weeks 2 days ago
27 weeks 2 days ago
49 weeks 3 days ago
1 year 1 week ago
1 year 3 weeks ago
1 year 3 weeks ago
1 year 5 weeks ago
1 year 10 weeks ago
1 year 10 weeks ago