View mode: basic / threaded / horizontal-split · Log in · Help
November 04, 2010
Spec#, nullables and more
Spec# is a Microsoft language, its development started in 2003, so it's not a new language. But both its specs and its implementation are unfinished still. Designing it is a long & hard task.

I have recently found a quite nice introduction to Spec#, "Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs" di K. Rustan M. Leino and Peter Muller (2009):
http://research.microsoft.com/en-us/um/people/leino/papers/krml189.pdf

Plus a nice Microsoft site that allows you to try it in interactive way, this is very good:
http://www.rise4fun.com/SpecSharp

Spec# is a "spinoff" of C# 2.0, it is designed to write more correct programs, using static verification too. This means that writing Spec# code is heavy, slow, and it may be a bit painful too. So it's meant only for code that needs to be reliable, not for quick scripts.

Spec# adds only few things to C# 2.0:
- Non-nullable types;
- Statically enforced Contract Programming syntax and semantics;
- A way to list what attributes are modified in a method (similar to my @outer).
- Checked exceptions (like Java ones).

It looks like a short list, but that list is both quite hard to implement, and changes a lot the idiomatic way you code, so it's not C# any more.

(The Spec# has produced two things: the Code Contracts library for C#4 and a C compiler that verifies the code).

Spec# looks very well designed and thought out, yet I don't see a lot of people interested in it. I presume the "Microsoft" tag drags it down a little. And probably not being really free doesn't help (maybe there is a partially open source version now). (And maybe people are not so interested in a language for low-bug-count programs).

Spec# isn't a system language, but a spinoff of Spec# named Sing# is a system language with low level features too (it has not GC-managed structs and pointers and some other things).

In Spec# contracts and assertions are verified statically. This changes a lot the way you code, and requires more brain from the programmer too. Reading the specs of Spec# it seems the designers have overdo it a bit here and there (better is not always better), you need to keep in mind some complex rules, and so on. I think Spec# is borderline usable, I have seen academic languages far more complex and hard to use than Spec#. For purposes where high integrity is important (where you may want to use Ada or even Spark) Spec# looks acceptable to me.

Several of the ideas I have suggested here or I have put in the D Bugzilla are already implemented (and well designed) in Spec#. I am happy.

The two main features of Spec# are its non-nullable types and its statically enforced Contract Programming. Its DbC uses a static verifier that I don't think will ever be added to DMD (despite eventually someone may try to write some static verifier for D). But DbC Spec# is well designed, and some of those ideas are useful to fix D design too.

Regarding Spec# non-nullable types I think they don't need a static verifier (beside the normal simple tests done by a static type system), and I think they are an additive change for D2, so they have a chance to be implementable for D3 too.

-----------------------------

Three quotations from the little tutorial (krml189.pdf):


Also, regardless of the compiler mode used, both inflections ? and ! are useful in the implementations of generic classes: if T is a type parameter constrained to be a reference type, then the naked name T stands for the actual type parameter (which might be a possibly-null type or a non-null type), T? stands for the possibly-null version of the type, and T! stands for the non-null version of the type.

-----------

Regardless of old, an in-parameter mentioned in a method contract always refers to the value of the parameter on entry (in other words, the fact that the language allows in-parameters to be used as local variables inside the method body has no effect on the meaning of the contract), and an out parameter always refers to the value of the parameter on exit; ref parameters, which are treated as copy-in copy-out, are sensitive to the use of old.

-----------

Non-null types express a special kind of invariant that needs to be established by each
constructor. The virtual machine initially sets all fields of a new object to zero-equivalent
values, in particular, fields of reference types to null. So before the new object has been
fully initialized, it would be unjustified to assume that non-null fields actually contain
non-null values.

Until the initialization of an object is completed, we say that the object is delayed, meaning
that it is in a raw state where we can rely neither on the non-nullness of its fields nor
on its object invariants. Moreover, field values of delayed objects are themselves allowed
to be delayed. By default, the this object is delayed inside constructors.

A delayed object is in general not allowed to escape from its constructor. However, sometimes
it is useful to call methods on delayed objects or to pass a delayed object as an
argument to a method call. This is permitted if the callee method or its parameter is
marked with the attribute [Delayed]. The consequence of this choice is that the method
is then not allowed to assume fields of non-null types to have non-null values, let alone
assume the object invariant to hold.(a)

An alternative is to mark the constructor with the attribute [NotDelayed]. This requires
that all non-null fields of the class be initialized before an explicit call of the superclass
(aka base class) constructor, base. A constructor can make a base call to a [NotDelayed]
superclass constructor only if it itself is marked as [NotDelayed]. A consequence of this
design is that after the base call, the this object is fully initialized and no longer delayed.
Therefore, it can be passed to methods without the [Delayed] attribute.

Fähndrich and Xia [7] describe the details of delayed objects. Examples for delayed objects
and explicit base calls can be found on the tutorial web page.

a) Any reference-valued parameter of a method, not just the receiver, can be marked with
[Delayed]. However, there is a bug in the current version of the program verifier that
makes the verification of methods with more than one [Delayed] parameter unsound.


The article also suggests the usage of a shorter form to cast to nullable or not nullable:
cast(@)someRef
cast(?)someRef


My reference issue:
http://d.puremagic.com/issues/show_bug.cgi?id=4571

Bye,
bearophile
November 05, 2010
Re: Spec#, nullables and more
bearophile Wrote:

> Plus a nice Microsoft site that allows you to try it in interactive way, this is very good:
> http://www.rise4fun.com/SpecSharp

D can do that too. We had those interactive versions in the newsrgoup. We saw no value in them.

> Spec# adds only few things to C# 2.0:
> - Non-nullable types;

The day D implements non-nullable types is the day I burn my copy of TDPL and stop using D. Why keep you pushin this crap. I don't want to hear about it. It doesn't improve my productivity at all.

> - Statically enforced Contract Programming syntax and semantics;

Too difficult to implement. Not worth it.

> - A way to list what attributes are modified in a method (similar to my @outer).

The compiler should do this itself.

> - Checked exceptions (like Java ones).

Oh god.. what were they smoking?


> My reference issue:
> http://d.puremagic.com/issues/show_bug.cgi?id=4571

Walter, please close this as wontfix. We don't need those. These extra runtime checks will slow down my code. I know myself when my pointer is null.

- G.W.
November 05, 2010
Re: Spec#, nullables and more
Gary Whatmore:

> I know myself when my pointer is null.

You are unusual then:
http://lambda-the-ultimate.org/node/3186

Bye,
bearophile
November 05, 2010
Re: Spec#, nullables and more
On 11/04/2010 03:44 PM, bearophile wrote:
> Spec# is a Microsoft language, its development started in 2003, so it's not a new language. But both its specs and its implementation are unfinished still. Designing it is a long&  hard task.
>
> I have recently found a quite nice introduction to Spec#, "Using the Spec# Language, Methodology, and Tools to Write Bug-Free Programs" di K. Rustan M. Leino and Peter Muller (2009):
> http://research.microsoft.com/en-us/um/people/leino/papers/krml189.pdf
>
> Plus a nice Microsoft site that allows you to try it in interactive way, this is very good:
> http://www.rise4fun.com/SpecSharp
>

hey, cool

stumbled on sing# a while ago and thought it was intriguing, or at least 
the fact that ms was using it to write an OS kernel
November 05, 2010
Re: Spec#, nullables and more
Ellery Newcomer:

> hey, cool
> 
> stumbled on sing# a while ago and thought it was intriguing, or at least 
> the fact that ms was using it to write an OS kernel

It contains a ton of new computer science ideas :-) So it's interesting regardless its applications. (If you don't keep yourself updated with new computer science ideas, you can't keep being a productive programmer for many years).

Bye,
bearophile
November 05, 2010
Re: Spec#, nullables and more
On Fri, 05 Nov 2010 14:43:48 +0300, Gary Whatmore <no@spam.sp> wrote:

> bearophile Wrote:
>
>> Plus a nice Microsoft site that allows you to try it in interactive  
>> way, this is very good:
>> http://www.rise4fun.com/SpecSharp
>
> D can do that too. We had those interactive versions in the newsrgoup.  
> We saw no value in them.
>
>> Spec# adds only few things to C# 2.0:
>> - Non-nullable types;
>
> The day D implements non-nullable types is the day I burn my copy of  
> TDPL and stop using D. Why keep you pushin this crap. I don't want to  
> hear about it. It doesn't improve my productivity at all.
>

Is anyone FORCING you to use non-nullable references?
What's the big deal?
November 05, 2010
Re: Spec#, nullables and more
On 11/05/2010 12:43 PM, Gary Whatmore wrote:
> bearophile Wrote:
>> - A way to list what attributes are modified in a method (similar to my @outer).
>
> The compiler should do this itself.

Doesn't make sense.

>> My reference issue:
>> http://d.puremagic.com/issues/show_bug.cgi?id=4571
>
> Walter, please close this as wontfix. We don't need those. These extra runtime checks will slow down my code. I know myself when my pointer is null.
>
>   - G.W.

How, exactly, do you know when your references are null? Without 
runtime checks, of course.
November 05, 2010
Re: Spec#, nullables and more
bearophile Wrote:

> Spec# adds only few things to C# 2.0:
> - Non-nullable types;

It's hard to tell, whether they fix anything. When you cast nullable to non-nullable, you get your runtime exception as usual, if you if out access to nullable (e.g. in delayed method), you get your runtime exception again or rather logical bug.
November 05, 2010
Re: Spec#, nullables and more
Pelle Månsson Wrote:

> On 11/05/2010 12:43 PM, Gary Whatmore wrote:
> > bearophile Wrote:
> >> - A way to list what attributes are modified in a method (similar to my @outer).
> >
> > The compiler should do this itself.
> 
> Doesn't make sense.
> 
> >> My reference issue:
> >> http://d.puremagic.com/issues/show_bug.cgi?id=4571
> >
> > Walter, please close this as wontfix. We don't need those. These extra runtime checks will slow down my code. I know myself when my pointer is null.
> >
> >   - G.W.
> 
> How, exactly, do you know when your references are null? Without 
> runtime checks, of course.

Good code design makes the null pointer exceptions go away. I carefully ponder what code goes where. Simple as that. That language just introduces a boatload of unnecessary cruft in forms of runtime null checks. I don't need to know the exact temporal location of nulls, it's enough if the code takes care of handling it at run time.
November 05, 2010
Re: Spec#, nullables and more
On 11/05/2010 02:39 PM, Kagamin wrote:
> bearophile Wrote:
>
>> Spec# adds only few things to C# 2.0:
>> - Non-nullable types;
>
> It's hard to tell, whether they fix anything. When you cast nullable to non-nullable, you get your runtime exception as usual, if you if out access to nullable (e.g. in delayed method), you get your runtime exception again or rather logical bug.

Getting the error early is actually a lot better than getting the error 
late.
« First   ‹ Prev
1 2 3 4 5
Top | Discussion index | About this forum | D home