Spec#

Categories:	Languages
Author:	Microsoft
Latest version:	1.0.20411
Description:	Programming system that is an attempt at a more cost effective way to develop and maintain high-quality software. The Spec# system consists of: - The Spec# programming language: 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# compiler. Integrated into Visual Studio, the compiler statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the contracts as metadata for consumption by downstream tools. - The Spec# static program verifier. Codenamed Boogie, this tool generates logical verification conditions from a Spec# program. Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it. 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. The Spec# programming system is being developed as a research project at Microsoft Research. Supports VS 2008 and 2005.
Added:	2008-04-24
Attributes:	[AddIn] [FreeVersionAvailable] [BuilfForDotNet2]