Stack Overflow
Stack Overflow

Questions tagged [spec#]

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.

Spec# home page at Microsoft research

16 questions
13
votes
11 answers

Why don't Java, C# and C++ have ranges?

Ada, Pascal and many other languages support ranges, a way to subtype integers. A range is a signed integer value which ranges from a value (first) to another (last). It's easy to implement a class that does the same in OOP but I think that…
Zen
  • 917
  • 1
  • 7
  • 20
6
votes
1 answer

Is Spec# stable enough to use?

Does anyone here use Spec# regularly? I would like to know if it is stable and powerful enough before I start using it everywhere. It looks like the syntax is influencing c# 4.0, which will hopefully make it easier to upgrade once 4.0 is released.…
cbp
  • 25,252
  • 29
  • 125
  • 205
4
votes
2 answers

What keywords/tools are there to help the compiler optimise

Often we're told things like, If you're calling a method with a return value that doesn't change, take it out of the loop. for example when writing code like: for(int i=0; i < Instance.ExpensiveNonChangingMethod(); i++) { // Stuff } I was…
George Duckett
  • 31,770
  • 9
  • 95
  • 162
4
votes
2 answers

Contract based Programming

Can someone explain the concepts that Spec# might be moving into C# 4.0, regarding Code Contracts? What are code contracts (Looks to be a compile time checking pattern) should I be excited about this? Am I correct in assuming that we move what…
FlySwat
  • 172,459
  • 74
  • 246
  • 311
4
votes
1 answer

Differences between Code Contract and Spec#

I want to implement the DBC in C#. I faced with the Spec# and Code Contract for it. What is the difference between Spec# and Code Contract?
tvahid
  • 210
  • 1
  • 9
3
votes
2 answers

How to define preconditions on extrinsic state using Code Contracts?

How do I place a precondition on the Invoke method in the following interface stating that the object denoted by ObjectId must exist?: interface IDeleteObjectCommand { Guid ObjectId { get; } void Invoke(); } Attempt #1 I already have a…
Lawrence Wagerfield
  • 6,471
  • 5
  • 42
  • 84
3
votes
1 answer

Whats wrong with non nullable objects?

I have been looking at DbC lately and Spec# which seem to have support for non nullable objects. Unfortunately Spec# seem to have been abandoned. Spec# seemed to have lots of nice language features built in so why was it abandoned? Would there be…
terjetyl
  • 9,497
  • 4
  • 54
  • 72
2
votes
1 answer

Spec#: is it good for me?

I'm working on a LOB framework, with an SL and MVC frontend, WCF backend, and few service modules that run on the server. I've been looking at the Spec#, to see if it helps me in any way. The non-nullable types and the checked exceptions are very…
TDaver
  • 7,164
  • 5
  • 47
  • 94
2
votes
1 answer

How to install Microsoft Spec# 2010

On MS-Research Microsoft has a C#-compatible language called Spec#. http://research.microsoft.com/en-us/projects/specsharp/ I found installer .msi only for Visual Studio…
OlimilOops
  • 6,747
  • 6
  • 26
  • 36
2
votes
1 answer

Exporting test scripts from Spec Explorer

Can someone explain how to use TestAdapter concept in Microsoft's Spec Explorer, to export tests..say, in .CSV format? I tried browsing through, but no clear answers anywhere. Prefer to get the solution in C#
HappyWaters
  • 39
  • 4
1
vote
2 answers

What do you think of the Managed Contract Tools library

I recently saw this video http://channel9.msdn.com/pdc2008/TL51/ about the managed Contract tools library which certainly looks very interesting. Sadly it seems they won't include this into the language itself which would have been more elegant as…
terjetyl
  • 9,497
  • 4
  • 54
  • 72
1
vote
1 answer

How to reset _version list to prevent duplicate states in Spec Explorer

I've made a Spec Explorer project that has a list as system variable. Almost in every rule this list is adapted to get the correct results. But when I explore my project I get duplicate states. If I compare these states the only difference I find…
Kyra
  • 173
  • 2
  • 16
1
vote
1 answer

Running the exploration result file of the TestSuite machine(Spec Explorer) in a Console Application

I'm having a problem while trying to follow a example of Spec Explorer, while using Visual Studio 2012. I've been following this link, but I get stuck on the running the Spec Explorer file with a Console Application. My problem starts at the next…
Kyra
  • 173
  • 2
  • 16
1
vote
1 answer

Initialize not null jagged array

I am currently studying computing at UCLAN and I have to write a program using Spec# and I need a 2 dimensial jagged array which can not be null. I know for a normal array I can declare it like this T![]! but when i want to declare it for a…
Vincenz Mössenböck
  • 453
  • 1
  • 4
  • 8
1
vote
2 answers

Check Active directory Group membership

How do i go about iterating a group to find out if a given user is a member of a group? I know i can use IsInRole on WindowsPrincipal object but for some reason it don't always work for me, it doesn't error out or throw exception but just return…
TheOCD
  • 161
  • 2
  • 3
  • 11
1
2