Ville det ikke vært fint om alle Java-klasser du bruker, inkludert dine egne, levde opp til sine løfter? Faktisk ville det ikke vært fint om du faktisk visste nøyaktig hva en gitt klasse lover? Hvis du er enig, les videre - Design by Contract og iContract kommer til unnsetning.
Merk: Kodekilden for eksemplene i denne artikkelen kan lastes ned fra Resources.
Design etter kontrakt
Design by Contract (DBC) programvareutviklingsteknikk sikrer programvare av høy kvalitet ved å garantere at hver komponent i et system lever opp til forventningene. Som utvikler som bruker DBC, spesifiserer du komponent kontrakter som en del av komponentens grensesnitt. Kontrakten spesifiserer hva komponenten forventer av kundene og hva kundene kan forvente av den.
Bertrand Meyer utviklet DBC som en del av Eiffels programmeringsspråk. Uansett opprinnelse er DBC en verdifull designteknikk for alle programmeringsspråk, inkludert Java.
Sentralt i DBC er forestillingen om en påstand - et boolsk uttrykk om tilstanden til et programvaresystem. Ved kjøretid vurderer vi påstandene ved spesifikke sjekkpunkter under systemets utførelse. I et gyldig programvaresystem evalueres alle påstander til sant. Med andre ord, hvis noen påstand evalueres som falsk, anser vi programvaresystemet som ugyldig eller ødelagt.
DBCs sentrale forestilling er noe knyttet til #assert
makro i programmeringsspråk C og C ++. Imidlertid tar DBC påstander et zillion nivå lenger.
I DBC identifiserer vi tre forskjellige typer uttrykk:
- Forutsetninger
- Postforhold
- Invarianter
La oss undersøke hver av dem mer detaljert.
Forutsetninger
Forutsetninger spesifiserer forhold som må holdes før en metode kan utføres. Som sådan blir de evaluert like før en metode kjøres. Forutsetninger involverer systemtilstanden og argumentene overført til metoden.
Forutsetninger spesifiserer forpliktelser som en klient til en programvarekomponent må oppfylle før den kan påberope seg en bestemt metode for komponenten. Hvis en forutsetning mislykkes, er det en feil i programvarekomponentens klient.
Postforhold
I motsetning til dette spesifiserer postconditions forhold som må holdes etter at en metode er fullført. Følgelig blir postconditions utført etter at en metode er fullført. Postforhold involverer den gamle systemtilstanden, den nye systemtilstanden, metodeargumentene og metodens returverdi.
Postconditions spesifiserer garantier som en programvarekomponent gir til sine kunder. Hvis en posttilstand brytes, har programvarekomponenten en feil.
Invarianter
En invariant angir en tilstand som må være når som helst en klient kan påberope seg et objekts metode. Invarianter er definert som en del av en klassedefinisjon. I praksis blir invarianter evaluert når som helst før og etter en metode på en hvilken som helst klasseinstans som utføres. Brudd på en invariant kan indikere en feil i enten klienten eller programvarekomponenten.
Påstander, arv og grensesnitt
Alle påstander som er spesifisert for en klasse og dens metoder gjelder også for alle underklasser. Du kan også spesifisere påstander om grensesnitt. Som sådan må alle påstander om et grensesnitt holde for alle klasser som implementerer grensesnittet.
iContract - DBC med Java
Så langt har vi snakket om DBC generelt. Du har sannsynligvis noen anelse nå hva jeg snakker om, men hvis du er ny i DBC, kan det fortsatt være litt tåkete.
I denne delen vil ting bli mer konkrete. iContract, utviklet av Reto Kamer, legger til konstruksjoner til Java som lar deg spesifisere DBC-påstandene vi snakket om tidligere.
grunnleggende om iContract
iContract er en forprosessor for Java. For å bruke den, behandler du først Java-koden din med iContract, og produserer et sett med dekorerte Java-filer. Deretter kompilerer du den dekorerte Java-koden som vanlig med Java-kompilatoren.
Alle iContract-direktiver i Java-kode ligger i klasse- og metodekommentarer, akkurat som Javadoc-direktiver. På denne måten sikrer iContract fullstendig bakoverkompatibilitet med eksisterende Java-kode, og du kan alltid kompilere Java-koden din direkte uten iContract-påstandene.
I en typisk programmets livssyklus vil du flytte systemet ditt fra et utviklingsmiljø til et testmiljø, deretter til et produksjonsmiljø. I utviklingsmiljøet vil du instrumentere koden din med iContract-påstander og kjøre den. På den måten kan du fange nylig introduserte bugs tidlig. I testmiljøet vil du kanskje fortsatt beholde hoveddelen av påstandene aktivert, men du bør ta dem ut av ytelseskritiske klasser. Noen ganger er det til og med fornuftig å holde noen påstander aktivert i et produksjonsmiljø, men bare i klasser som definitivt ikke er kritiske for systemets ytelse. iContract lar deg eksplisitt velge klassene du vil instrumentere med påstander.
Forutsetninger
I iContract plasserer du forutsetninger i en metodehode ved hjelp av @pre
direktivet. Her er et eksempel:
/ ** * @pre f> = 0.0 * / public float sqrt (float f) {...}
Eksempelets forutsetning sikrer at argumentasjonen f
av funksjon sqrt ()
er større enn eller lik null. Kunder som bruker denne metoden er ansvarlige for å overholde denne forutsetningen. Hvis de ikke gjør det, vi som implementører av sqrt ()
er rett og slett ikke ansvarlige for konsekvensene.
Uttrykket etter @pre
er et Java Boolean-uttrykk.
Postforhold
Postforhold legges også til toppteksten til metoden de tilhører. I iContract er @post
direktivet definerer posttilstander:
/ ** * @pre f> = 0.0 * @post Math.abs ((return * return) - f) <0.001 * / public float sqrt (float f) {...}
I vårt eksempel har vi lagt til en posttilstand som sørger for at sqrt ()
metoden beregner kvadratroten av f
innenfor en spesifikk feilmargin (+/- 0,001).
iContract introduserer noen spesifikke notasjoner for postconditions. Først av alt, komme tilbake
står for returverdien av metoden. Ved kjøretid vil dette bli erstattet av metodens returverdi.
Innenfor postconditions er det ofte behov for å skille mellom verdien av et argument før gjennomføring av metoden og etterpå, støttet i iContract med @pre
operatør. Hvis du legger til @pre
til et uttrykk i en posttilstand, vil det bli evaluert basert på systemtilstanden før metoden kjøres:
/ ** * Legg et element til en samling. * * @post c.size () = [email protected] () + 1 * @post c.contains (o) * / public void append (Collection c, Object o) {...}
I koden ovenfor spesifiserer den første posttilstanden at størrelsen på samlingen må vokse med 1 når vi legger til et element. Uttrykket c @ pre
refererer til samlingen c
før gjennomføring av legge til
metode.
Invarianter
Med iContract kan du spesifisere invarianter i toppteksten til en klassedefinisjon:
/ ** * Et positivt heltall er et heltall som garantert vil være positivt. * * @inv intValue ()> 0 * / klasse PositiveInteger utvider heltall {...}
I dette eksemplet garanterer invarianten at Positivt heltall
Verdien er alltid større enn eller lik null. Denne påstanden blir sjekket før og etter gjennomføring av en hvilken som helst metode i den klassen.
Object Constraint Language (OCL)
Selv om påstandsuttrykkene i iContract er gyldige Java-uttrykk, er de modellert etter et delsett av Object Constraints Language (OCL). OCL er en av standardene som vedlikeholdes og koordineres av Object Management Group, eller OMG. (OMG tar seg av CORBA og relaterte ting, hvis du savner forbindelsen.) OCL var ment å spesifisere begrensninger innen objektmodelleringsverktøy som støtter Unified Modeling Language (UML), en annen standard beskyttet av OMG.
Fordi iContract-uttrykkespråket er modellert etter OCL, gir det noen avanserte logiske operatører utover Javas egne logikkoperatører.
Kvantifiseringsmidler: for alt og eksisterer
iContract støtter for alle
og eksisterer
kvantifiserere. De for alle
kvantifiser angir at en betingelse skal holde seg gjeldende for hvert element i en samling:
/ * * @variant for alle I-ansatte e i get-ansatte () | * getRooms (). inneholder (e.getOffice ()) * /
Ovenstående invariant spesifiserer at hver ansatt som returneres av getEmployees ()
har et kontor i samlingen av rom returnert av getRooms ()
. Bortsett fra for alle
nøkkelord, syntaksen er den samme som en eksisterer
uttrykk.
Her er et eksempel på bruk av eksisterer
:
/ ** * @post eksisterer IRoom r i getRooms () | r.isAvailable () * /
Denne posttilstanden angir at samlingen returnert av etter at den tilknyttede metoden er utført getRooms ()
vil inneholde minst ett tilgjengelig rom. De eksisterer
fortsetter Java-typen for samlingselementet - IR-rom
i eksemplet. r
er en variabel som refererer til ethvert element i samlingen. De i
nøkkelord følges av et uttrykk som returnerer en samling (Oppregning
, Array
, eller Samling
). Dette uttrykket etterfølges av en vertikal stolpe, etterfulgt av en tilstand som involverer elementvariabelen, r
i eksemplet. Ansette eksisterer
kvantifiserende når en betingelse må oppfylle minst ett element i en samling.
Både for alle
og eksisterer
kan brukes på forskjellige typer Java-samlinger. De støtter Oppregning
s, Array
s, og Samling
s.
Implikasjoner: innebærer
iContract tilbyr tilsier
operatøren for å spesifisere begrensninger for skjemaet, "Hvis A holder, så må B også holde." Vi sier "A innebærer B." Eksempel:
/ ** * @invariant getRooms (). isEmpty () innebærer getEmployees (). isEmpty () // ingen rom, ingen ansatte * /
Den invarianten uttrykker det når getRooms ()
samlingen er tom, den getEmployees ()
samlingen må også være tom. Merk at den ikke spesifiserer at når getEmployees ()
er tom, getRooms ()
må være tom også.
Du kan også kombinere de logiske operatorene som nettopp ble introdusert for å danne komplekse påstander. Eksempel:
/ ** * @variant for alle IE-ansatte e1 i getEmployees () | * for alle IEmployee e2 i getEmployees () | * (e1! = e2) innebærer e1.getOffice ()! = e2.getOffice () // et enkelt kontor per ansatt * /
Begrensninger, arv og grensesnitt
iContract formerer begrensninger langs arv og grensesnittimplementeringsforhold mellom klasser og grensesnitt.
Anta klasse B
utvider klassen EN
. Klasse EN
definerer et sett med invarianter, forutsetninger og etterbetingelser. I så fall klassens invarianter og forutsetninger EN
gjelder klassen B
også, og metoder i klassen B
må tilfredsstille de samme postforholdene som klassen EN
tilfredsstiller. Du kan legge til mer restriktive påstander i klassen B
.
Den nevnte mekanismen fungerer også for grensesnitt og implementeringer. Anta EN
og B
er grensesnitt og klasse C
implementerer begge deler. I så fall, C
er underlagt invarianter, forutsetninger og etterbetingelser for begge grensesnittene, EN
og B
, så vel som de som er definert direkte i klassen C
.
Vokt dere for bivirkninger!
iContract vil forbedre kvaliteten på programvaren din ved å la deg fange mange mulige feil tidlig. Men du kan også skyte deg selv i foten (det vil si introdusere nye feil) ved hjelp av iContract. Det kan skje når du påkaller funksjoner i iContract-påstandene dine som gir bivirkninger som endrer systemets tilstand. Det fører til uforutsigbar oppførsel fordi systemet vil oppføre seg annerledes når du kompilerer koden din uten iContract-instrumentering.
Stabeleksemplet
La oss se på et komplett eksempel. Jeg har definert Stable
grensesnitt, som definerer de kjente operasjonene til min favoritt datastruktur:
/ ** * @inv! isEmpty () innebærer topp ()! = null // ingen nullobjekter er tillatt * / offentlig grensesnitt Stack {/ ** * @pre o! = null * @post! isEmpty () * @post topp () == o * / ugyldig trykk (Objekt o); / ** * @pre! isEmpty () * @post @return == top () @ pre * / Object pop (); / ** * @pre! isEmpty () * / Object top (); boolsk isEmpty (); }
Vi tilbyr en enkel implementering av grensesnittet:
importer java.util. *; / ** * @inv isEmpty () innebærer elements.size () == 0 * / offentlig klasse StackImpl implementerer Stack {private final LinkedList elements = new LinkedList (); public void push (Object o) {elements.add (o); } public Object pop () {final Object popped = top (); elements.removeLast (); retur poppet; } public Object top () {return elements.getLast (); } offentlig boolsk isEmpty () {return elements.size () == 0; }}
Som du kan se, er Stable
implementeringen inneholder ingen iContract-påstander. Snarere blir alle påstander gjort i grensesnittet, noe som betyr at komponentkontrakten til Stack er definert i grensesnittet i sin helhet. Bare ved å se på Stable
grensesnitt og dets påstander, Stable
oppførsel er fullstendig spesifisert.
Nå legger vi til et lite testprogram for å se iContract i aksjon:
public class StackTest {public static void main (String [] args) {final Stack s = new StackImpl (); s.push ("en"); s.pop (); s.push ("to"); s.push ("tre"); s.pop (); s.pop (); s.pop (); // får en påstand til å mislykkes}}
Deretter kjører vi iContract for å bygge stackeksemplet:
java -cp% CLASSPATH%; src; _contract_db; instr com.reliablesystems.iContract.Tool -Z -a -v -minv, pre, post> -b "javac -classpath% CLASSPATH%; src" -c "javac -classpath % CLASSPATH%; instr "> -n" javac -classpath% CLASSPATH%; _ contract_db; instr "-oinstr / @ p / @ f. @ E -k_contract_db / @ p src / *. Java
Uttalelsen ovenfor garanterer en liten forklaring.