Spec#

using System;

static class Program {
	private static void Main(string[]! args) requires forall{ string s in args; s != null }; {
		string result = GetString();

		// string! badNonNullResult = result;		// compiliert nicht

		if( result != null ) {
			string! nonNullResult = result;			// compiliert schon
			nonNullResult = nonNullResult.Substring(1);
			PrintObject(nonNullResult);
		}

		Console.In.ReadLine();
	}

	private static string GetString() ensures result != "foo"; {	// möglicher crash zur laufzeit
		string blubb = new Random().Next(2) == 0  ?  "foo" : null;
		return blubb;
	}

	private static void PrintObject(object! obj) {
		if( obj == null )		// Ohje, keine Warnung...
			return;

		Console.Out.WriteLine(obj.ToString());
	}
}

Wie findet ihr die Möglichkeit, solche Verträge in die Methodensignaturen zu schreiben? Eigentlich nicht so schlecht, meiner bescheidenen Meinung nach. Es ist halt ein bisschen schade, dass das meiste erst zur Laufzeit verifiziert wird, also ist keine große Magie dahinter. Aber zumindest schreibt man etwas klar hin, wofür sonst if( ... ) throw new ArgumentException(...); mitten im Code stehen muss. Und der null-check ist wenigstens zur compile-zeit.

Spec# bietet auch Sprachmittel für Objekt-Invarianten.

http://research.microsoft.com/specsharp/

Vielleicht hält sowas Einzug in einer der nächsten .Net Sprachen...

DrGreenthumb

Optimizer schrieb:

Wie findet ihr die Möglichkeit,...

ist natürlich schön, wenn der Code gleich den Kommentar bildet, aber in dieser verhunzten C/++Java-Syntax kommt das irgendwie uncool. Besonders die Main-Signatur.
Ich fande zB. assert_argument oder -_result innerhalb der Funktion hübscher.

Aber ich blicke auch nicht wirklich durch dein Beispiel...

Jester

Gefällt mir eigentlich recht gut. Schön wäre es, auch für Klassen noch Invarianten definieren zu können.

Daß die Syntax die Spezifikation etwas aus dem Code herauslöst ist aus der Sicht heraus praktisch, daß man beide dann möglicherweise getrennt verarbeiten kann. Es gibt ja inzwischen auch schon ein paar Tools, die teilweise versuchen, diese Aussagen tatsächlich zu beweisen, sodaß der Code auf die checks verzichten kann, weil die Fälle bewiesen nicht auftauchen.

Jester schrieb:

Gefällt mir eigentlich recht gut. Schön wäre es, auch für Klassen noch Invarianten definieren zu können.

Wenn ich dich richtig verstehe geht das:

class Word {
    private string! line; private int start; public int length;
    invariant 0 <= start && 0 <= length;
    invariant start + length <= line.Length;

    public Word(string! line, int start, int length)
            requires 0 <= start && 0 <= length;
            requires start + length <= line.Length;
            ensures inv; {
        this.line = line; this.start = start; this.length = length;
        base();
        EndExpose();    // aktiviert die Invarianten-Prüfung
    }
}

Jester

Hey, das sieht nett aus.

Warum steht da "ensures inv"? Ist inv eine spezielle invariante, oder ist das ein fest stehender Ausdruck? Was bedeutet ensures genau? Daß die Invariante erhalten wird, oder daß sie hergestellt wird?

edit: Okay, hab's kapiert. Hab mir die Slides angeschaut.

Helium

Naja, die non-Null-Typen da kommen mir doch bekannt vor (siehe Nice), also nichts neues. (Prinzipiell könnte man ja sogar sagen, dass es in den meisten funktionalen Sprachen sogar üblich ist non-Null-Types zu verwenden und Null-Types dann erst durch sowas wie Options "nachzubauen".)

Dann kommen ein paar DbC-Konstrukte, die es überall gibt (Eiffel, etc., sogar in D). Aber dann wird es interessant, weil das Konzept erweitert wird und zwar mit mir unbekanntem
Beim schnellen Durchklicken der Präsentation habe ich da auch einiges noch nicht so 100% verinnerlicht, werde es mir aber auf jeden Fall nochmal angucken (ednlich nochmal was interessantes).