Spec#
Get flash to fully experience Pearltrees
Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about object invariants even in the presence of callbacks and multi-threading. Spec# is a research vehicle that has been used to explore specifications and the dynamic/static tools that make use of them. The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. Spec# is pronounced "Spec sharp" and can be written (and searched for) as the "specsharp" or "Spec# programming system".
Spec# - Microsoft Research
Model-based Testing with SpecExplorer
Encode a system's intended behavior (its specification) in machine-executable form (as a "model program"). The model program typically does much less than the implementation; it does just enough to capture the relevant states of the system and show the constraints that a correct implementation must follow. The goal is to specify from a chosen viewpoint what the system must do, what it may do and what it must not do. Explore the possible runs of the specification-program as a way to systematically generate test suites.
Spec# for Visual Studio 2008
Spec# is an experimental language that extends C# (version 2) with several design-by-contract features. The new features of Spec# include a non-null type system, method pre- and post-conditions, loop invariants, and object invariants. The Spec# Programming System provides design-time checking, run-time checking, and a static verifier. This version of Spec# works with Visual Studio 2008.
Spec#: Adding Contracts to C#
Microsoft Spec# is a strict superset of Microsoft Visual C# that adds the idea of code contracts. Code contracts are designed to capture programmer intentions about how methods and data should be used, such as method preconditions, postconditions, and object invariants. Join this webcast and learn how the Spec# compiler emits run-time checks that enforce the contracts and how the Spec# program verifier uses theorem-proving technology to check the consistency statically between a program and its contracts. Spec# is integrated into Microsoft Visual Studio .NET 2003 and is meant to help programmers write correct software and to make explicit the correct usage of APIs for clients. Presenter: Mike Barnett, Research Software Design Engineer, Microsoft Corporation
I've been blogging about the Comega language on my blog earlier (and will continue to do so in the near future), which is a superset of the C# language that focuses primarily on object/relational/hierarchical data manipulation and mapping on the one hand and concurrency language extensions on the other hand. Part of the features of Comega are already available in C# 2.0 (e.g. the yield statement, anonymous delegates and more deeply closures). In this post I'm introducing you to another Microsoft Research project called Spec#, which is a superset of the C# language too.
An introduction to Spec#
Scott Hanselman is a former professor, former Chief Architect in finance, now speaker, consultant, father, diabetic, and Microsoft employee. I promise not to waste your time. Building quality software is never easy. It requires skills and imagination. We cannot promise to improve your skills, but when it comes to User Interface and developer tools, we can provide the building blocks to take your application a step closer to your imagination.
Hanselminutes - Spec#
Here is another video in the videos from altdotnet. We had Rustan and Mike of the spec# come out from their cave (j/k) at MSR to talk about spec#, boogie, and the future of compile time proving!
Spec# Session
The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. Spec# is pronounced "Spec sharp" and can be written (and searched for) as the "specsharp" or "Spec# programming system". The Spec# system consists of: The Spec# programming language .
Contract Oriented Programming and Spec#
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.
Spec#
Spec# and ideas for C# 4.0
It is not only the runtime aspects of spec# that are exiting. It is the amazing level of static analysis that they have implemented that at compile time validates (across many method boundaries) that requirements are uphold. C# has really evolved a lot in the last two iterations (especially in 3.0), and think this fast evolution has given it a good edge compared to other static languages (java). But why stop now? Here are a few more things I would like in C# 4.0 :) Extensible compilation pipeline:
Spec# is a programming language with specification language features that extends the capabilities of the C# programming language with Eiffel -like contracts , including object invariants , preconditions and postconditions. Like ESC/Java , it includes a static checking tool based on a theorem prover that is able to statically verify many of these invariants. It also includes a variety of other minor extensions to the language, such as non-null reference types. The code contracts API in the .NET Framework 4.0 has evolved with Spec#. Microsoft Research developed both Spec# and C# ; in turn, Spec# serves as the foundation of the Sing# programming language, which Microsoft Research also developed.