Specificeren versus verifiëren

 
27 februari 2008

Unittesten is iets wat we inmiddels allemaal kennen. In een methode als Test Driven Development hebben we zelfs het doel om eerst de testen te specificeren en daarna de code (het gedrag) te implementeren. Dat klinkt goed en werkt ook goed als de applicatie architectuur het ondersteund. Dat we binnen Sogyo volgens een domein gedreven architectuur werken is inmiddels wel bekend en daar past deze stijl ook erg goed bij.

Op dit moment is er een interessante ontwikkeling gaande die vooral in de Ruby-wereld al uitgebreid toegepast wordt en met groot succes. Het gaat om specificatietalen. In zijn artikel A new look at Test Driven Development beschrijft Dave Atels op een beeldige manier wat het verschil is tussen de specificatietalen en testgedrevenheid. In essentie komt het neer op vooraf specificeren versus het achteraf verifiëren. Dan zou je kunnen zeggen “lekker spannend”. Echter wat het wat mij betreft interessant maakt is het feit dat je met specificatietalen dus vooraf formeel kunt beschrijven waaraan de implementatie moet voldoen. Je specifieert dus in een executeerbare taal. (Puur technisch gezien gelijkwaardig aan Unittest technieken). Dat zegt natuurlijk ook iets over de (lage) abstractie waarin de specificatie plaatsvindt. Die zou in dit geval op scenario niveau binnen een Use Case moeten liggen om concreet genoeg te zijn. Dat is mooi!
We hebben recent voor een klant een platform gerealiseerd waarin de ontkoppeling van het domein met de presentatie services plaatsvindt door “contracten” (of views op het domein) op Use Case niveau te definiëren. Dat betekent dus dat je een specificatietaal in moet kunnen zetten om tests voor deze contracten vooraf te schrijven. Interessant terein om verder te ontdekken.

Overigens zijn er best veel ontwikkelingen op gebied van specificatietalen. RSpec is in de Ruby-wereld een heel bekende. JBehave en NBehave lijken goede alternatieven voor Java en .NET. Maar ook Microsoft zelf is druk bezig met een implementatie. Je moet er nog even voor op zoek binnen Microsoft Research, maar Spec# klinkt veelbelovend.


Werken met ?
Kijk dan bij onze mogelijkheden voor zowel starters als ervaren engineers.


Categorieën: Project- & procesmanagement, Development

Tags: ,


Reacties (3)

  • Alex Kuiper schreef:

    IK heb hier vanuit m’n studie ook wat mee gespeeld…. er is zeker vanuit de academische hoek nogal wat aandacht voor het specifieren.

    Een redelijk vergaand systeem hiervoor is Alloy (http://alloy.mit.edu/) waarbij het je aannames kan loslaten op een formele specificatie, en Alloy dan gaat zoeken naar een tegenvoorbeeld. Dit is echter een nogal wiskundige benadering die ik nog niet zo snel toegepast zie worden in projecten… tenzij je de spreekwoordelijke kerncentrale aan het bouwen bent natuurlijk :)

    Wat ik zelf erg interessant vond was RushCheck voor Ruby… hierbij geef je een aantal voorwaarden waar test-objecten aan moeten voldoen, en vervolgens wordt je test 1000x gedraaid met een hele serie random input.

    Je vindt daarmee al snel veel van de vreemde randgevallen die je anders gemist zou hebben.

    Geplaatst op 01 april 2008 om 16:07 Permalink

  • Eens dat specificatietalen op zichzelf helemaal niet nieuw zijn. Ze zijn gebaseerd op ideeën zoals Bertrand Meyer die met “design by contract” heeft geïntroduceerd en geïmplementeerd in Eiffel. En ja het klopt dat specificatietalen specifieker zijn dan unit tests.
    Waar het om gaat is de redenatie dat je eerst je specificatie gaat maken en daarna pas je de implementatie. Zoals je beschrijft “de weg andersom”. Ook dit is niet nieuw . Als we TTD “netjes” doen dan maken we eerst de test en dan de implementatie die de test tot een positief resultaat brengt.
    In veel projecten zie je echter toch dat de unit tests achteraf geschreven worden. Het zijn dan ook de ontwikkelaars die de units dan beschrijven. Met de specificatietalen is het interessante dat juist de specs door de domeindeskundige beschreven kunnen worden. Dat vind ik erg interessant.
    In het project waaraan ik refereer hebben we zelfs meerdere niveaus waarop je die specificaties zou kunnen leggen. Van use case niveau met verschillende scenario’s tot op domeinniveau. Daarmee zijn voordelen te halen doordat je verschillende mensen op verschillende abstractieniveau’s met de software ontwikkeling aan de gang laat gaan. Echter door de onderdelen specifiek te beschrijven sluiten ze beter op elkaar.

    Geplaatst op 29 februari 2008 om 15:18 Permalink

  • Jasper Stein schreef:

    Het idee van verifiëren vs. specificeren is verre van nieuw, maar ook verre van oninteressant :-) Naar ik begrijp heeft de taal Eiffel al flink veel ervaring met specificeren, omdat het daar nl. onderdeel van de taal zelf is, ipv. een laag erbovenop.

    Ook voor Java bestaan er specificatietalen; oa. JML is er een (maar er zijn er meer). Hiermee zet je de specificatie in een stuk commentaar boven je code; met declaraties als \requires en \ensures kan je dan bijv. je pre- en post-condities voor je functie aangeven.

    Het idee is dat een externe tool nu de specificatie en de bijbehorende code pakt, de code omzet naar een model binnen een formele stellingbewijzer zoals bijv. de bewijsassistent Coq, en de specificatie omzet naar formele beweringen over dat model, in de taal van de stellingbewijzer. Het is dan vervolgens aan de programmeur om binnen het formele systeem van de stellingbewijzer te bewijzen dat de gegenereerde beweringen ook daadwerkelijk kloppen. Ervan uitgaande dat de tool correcte modellen en beweringen genereert, heb je dan ook bewezen dat jouw code zich aan de meegegeven specificatie voldoet.

    Je opmerking over ‘Puur technisch gezien gelijkwaardig aan Unittest-technieken’ is dan ook NIET waar: een formele specificatie is veel STERKER! Dat komt namelijk omdat je in je specificatie niet alleen aangeeft (zoals bij Unittests) dat bij +deze+ specifieke invoer, +dat+ resultaat wordt verwacht, maar dat bij +alle+ invoer van de vorm xyz, dit-en-dat het resultaat moet zijn.

    Juist doordat je het over hele klassen van invoer hebt, kan het (itt bij Unittests) niet voorkomen dat je randgevallen over het hoofd ziet.

    Overigens is de weg andersom ook mogelijk: in Coq is het bijv. mogelijk om eerst een bewering op te schrijven in de trant van “er is een functie met een argument van type T en uitvoertype X, met de eigenschap dat …x-y-z… geldt”, vervolgens binnen het systeem te bewijzen dat die bewering klopt, en daaruit vervolgens het bijbehorende programma te +extraheren+ (genereren, zo je wilt) in een van de daarvoor ondersteunde talen.

    Java en C# zijn daar nog niet bij; dit soort onderzoek (want dat is het nog steeds voor een deel) speelt zich vooral af in de functionele talen-hoek, maar wie Haskell, OCaml of Scheme begrijpt (zijn het geloof ik), die kan hier leuke dingen mee bereiken.

    Jasper Stein

    Geplaatst op 28 februari 2008 om 21:14 Permalink