Spec#, nullables and more

[bearophile]

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