Note
Access to this page requires authorization. You can try signing in or changing directories.
Access to this page requires authorization. You can try changing directories.
From the research web site:
The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. The system consists of:
- A programming methodology, which includes a sound treatment of object invariants in object-oriented programs.
- The Spec# programming language, which is a superset of C# and adds things like non-null types, checked exceptions, method contracts (like pre- and postconditions), and object invariants.
- The Spec# compiler, which is integrated into the Microsoft Visual Studio development environment, statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the specifications in metadata for consumption by the program verifier.
- The Spec# static program verifier, which translates programs into logical verification conditions, which are passed to an automatic theorem prover.
- An interface to the SpecExplorer tool for test generation and model-based testing.
More info: https://research.microsoft.com/SpecSharp/
If you've ever read the Pragmatic Programmer or done contract-based programming before with tools like iContract, you'll instantly see the value of pre- and post- conditions for code.