This post originated from an RSS feed registered with .NET Buzz
by -.
Original Post: Spec# -
Feed Title: Norbert Eder - Living .NET
Feed URL: http://feeds.feedburner.com/NorbertEder-Livingnet
Feed Description: Copyright (c)2005, 2006 by Norbert Eder
Bei Spec# handelt es sich um eine Erweiterung von C#. C# wird dabei um beispielsweise Pre- und Postconditions adaptiert.
The Spec# programming language. Spec# is an extension of the object-oriented language 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 the Microsoft Visual Studio development environment for the .NET platform, 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. This component (codenamed Boogie) 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.
Wer sich das einmal genauer ansehen möchte, der findet einen guten Ausgangspunkt auf Spec# Home.
Previous Topic
