Design efter kontrakt - Design by contract

En design efter kontraktordning

Design efter kontrakt ( DbC ), også kendt som kontraktprogrammering , programmering efter kontrakt og design-by-contract programmering , er en tilgang til design af software .

Det foreskriver, at softwaredesignere bør definere formelle , præcise og verificerbare grænsefladespecifikationer for softwarekomponenter , der udvider den almindelige definition af abstrakte datatyper med forudsætninger , efterbetingelser og invarianter . Disse specifikationer betegnes som "kontrakter" i overensstemmelse med en konceptuel metafor med forretningskontrakters betingelser og forpligtelser.

DbC -tilgangen forudsætter, at alle klientkomponenter, der påkalder en operation på en serverkomponent, opfylder de forudsætninger, der er angivet som nødvendige for denne operation.

Hvor denne antagelse betragtes som for risikabel (som i multikanal eller distribueret computing ), tages den omvendte tilgang , hvilket betyder, at serverkomponenten tester, at alle relevante forudsætninger er opfyldt (før eller under behandling af klientkomponentens anmodning) og svarer med en passende fejlmeddelelse, hvis ikke.

Historie

Begrebet blev opfundet af Bertrand Meyer i forbindelse med hans design af programmeringssproget Eiffel og først beskrevet i forskellige artikler, der startede i 1986 og de to på hinanden følgende udgaver (1988, 1997) af hans bog Object-Oriented Software Construction . Eiffel Software ansøgte om varemærkeregistrering for Design by Contract i december 2003, og det blev givet i december 2004. Den nuværende ejer af dette varemærke er Eiffel Software.

Design efter kontrakt har sine rødder i arbejdet med formel verifikation , formel specifikation og Hoare -logik . De oprindelige bidrag omfatter:

Beskrivelse

Den centrale idé med DbC er en metafor om, hvordan elementer i et softwaresystem samarbejder med hinanden på grundlag af gensidige forpligtelser og fordele . Metaforen kommer fra erhvervslivet, hvor en "kunde" og en "leverandør" er enige om en "kontrakt", der for eksempel definerer, at:

  • Leverandøren skal levere et bestemt produkt (forpligtelse) og er berettiget til at forvente, at kunden har betalt sit gebyr (ydelse).
  • Kunden skal betale gebyret (forpligtelsen) og er berettiget til at få produktet (fordelen).
  • Begge parter skal opfylde visse forpligtelser, f.eks. Love og regler, der gælder for alle kontrakter.

På samme måde, hvis metoden for en klasse i objektorienteret programmering giver en bestemt funktionalitet, kan den:

  • Forvent, at en bestemt betingelse garanteres ved indtastning af ethvert klientmodul, der kalder det: Metodens forudsætning - en forpligtelse for kunden og en fordel for leverandøren (selve metoden), da den frigør den fra at skulle håndtere sager uden for forudsætningen.
  • Garanter en bestemt ejendom ved udgang: Metodens postkondition - en forpligtelse for leverandøren og naturligvis en fordel (den største fordel ved at kalde metoden) for kunden.
  • Bevar en bestemt ejendom, antaget ved indrejse og garanteret ved udgang: klasse invariant .

Kontrakten svarer semantisk til en Hoare -triple, der formaliserer forpligtelserne. Dette kan opsummeres af de "tre spørgsmål", som designeren gentagne gange skal besvare i kontrakten:

  • Hvad forventer kontrakten?
  • Hvad garanterer kontrakten?
  • Hvad fastholder kontrakten?

Mange programmeringssprog har faciliteter til at komme med påstande som disse. DbC anser imidlertid disse kontrakter for at være så afgørende for softwarens korrekthed, at de bør indgå i designprocessen. DbC går faktisk ind for at skrive påstandene først . Kontrakter kan skrives ved hjælp af kodekommentarer , håndhæves af en testsuite eller begge dele, selvom der ikke er særlig sprogstøtte til kontrakter.

Tanken om en kontrakt strækker sig ned til metode/procedureniveau; kontrakten for hver metode vil normalt indeholde følgende oplysninger:

Underklasser i en arv hierarki får lov til at svække forudsætninger (men ikke styrke dem) og styrke postconditions og invarianter (men ikke svække dem). Disse regler tilnærmer adfærdsundertyping .

Alle klasseforhold er mellem klientklasser og leverandørklasser. En klientklasse er forpligtet til at foretage opkald til leverandørfunktioner, hvor leverandørens resulterende tilstand ikke krænkes af klientopkaldet. Efterfølgende er leverandøren forpligtet til at oplyse en returtilstand og data, der ikke overtræder klientens statskrav.

For eksempel kan en leverandørdatabuffer kræve, at data er til stede i bufferen, når en slettefunktion kaldes. Efterfølgende garanterer leverandøren over for klienten, at når en slettefunktion er færdig med sit arbejde, vil dataelementet faktisk blive slettet fra bufferen. Andre designkontrakter er begreber om klasse invariant . Klassen invariant garanterer (for den lokale klasse), at klassens tilstand vil blive opretholdt inden for specificerede tolerancer ved afslutningen af ​​hver funktionsudførelse.

Ved brug af kontrakter bør en leverandør ikke forsøge at verificere, at kontraktbetingelserne er opfyldt - en praksis kendt som offensiv programmering - den generelle idé er, at koden skal "fejle hårdt", idet kontraktverifikation er sikkerhedsnettet.

DbC's "fail hard" ejendom forenkler fejlretning af kontraktadfærd, da den tilsigtede adfærd for hver metode er klart specificeret.

Denne tilgang adskiller sig væsentligt fra den defensive programmering , hvor leverandøren er ansvarlig for at finde ud af, hvad han skal gøre, når en forudsætning brydes. Oftere end ikke kaster leverandøren en undtagelse for at informere klienten om, at forudsætningen er brudt, og i begge tilfælde - både DbC og defensiv programmering - skal kunden finde ud af, hvordan han skal reagere på det. I sådanne tilfælde gør DbC leverandørens job lettere.

Design efter kontrakt definerer også kriterier for korrekthed for et softwaremodul:

  • Hvis klasse invariant OG forudsætningen er sand, før en leverandør kaldes af en klient, så vil invarianten OG postbetingelsen være sand, efter at servicen er afsluttet.
  • Når der foretages opkald til en leverandør, bør et softwaremodul ikke krænke leverandørens forudsætninger.

Design efter kontrakt kan også lette genbrug af kode, da kontrakten for hvert stykke kode er fuldt dokumenteret. Kontrakterne for et modul kan betragtes som en form for softwaredokumentation for modulets adfærd.

Ydelsesmæssige konsekvenser

Kontraktsbetingelser bør aldrig krænkes under udførelse af et fejlfrit program. Kontrakter kontrolleres derfor typisk kun i fejlretningstilstand under softwareudvikling. Senere ved frigivelse deaktiveres kontraktscheckene for at maksimere ydelsen.

I mange programmeringssprog implementeres kontrakter med påstand . Asserts kompileres som standard væk i frigivelsestilstand i C/C ++ og deaktiveres på samme måde i C# og Java.

Lancering af Python-tolken med "-O" (til "optimering") som et argument vil ligeledes medføre, at Python-kodegeneratoren ikke udsender nogen bytecode for asserts.

Dette eliminerer effektivt driftstidsomkostningerne for asserts i produktionskoden-uanset antallet og beregningsomkostningerne for asserts, der bruges i udviklingen-da ingen sådanne instruktioner vil blive inkluderet i produktionen af ​​compileren.

Forholdet til softwaretest

Design efter kontrakt erstatter ikke regelmæssige teststrategier, f.eks. Enhedstest , integrationstest og systemtest . Den supplerer snarere ekstern testning med interne selvtests, der kan aktiveres både for isolerede test og i produktionskode under en testfase.

Fordelen ved interne selvtest er, at de kan opdage fejl, før de viser sig som ugyldige resultater observeret af klienten. Dette fører til tidligere og mere specifik fejlopdagelse.

Anvendelsen af ​​påstande kan betragtes som en form for testorakel , en måde at teste designet ved kontraktimplementering.

Sprogstøtte

Sprog med native support

Sprog, der implementerer de fleste DbC -funktioner, inkluderer:

Sprog med tredjeparts support

Forskellige biblioteker, preprocessorer og andre værktøjer er blevet udviklet til eksisterende programmeringssprog uden native design ved hjælp af kontraktstøtte:

Se også

Noter

Bibliografi

  • Mitchell, Richard og McKim, Jim: Design by Contract: f.eks . Addison-Wesley, 2002
  • En wikibog, der beskriver DBC tæt på den originale model.
  • McNeile, Ashley: En ramme for adfærdskontrakters semantik . Proceedings of the Second International Workshop on Behavior Modeling: Foundation and Applications (BM-FA '10). ACM, New York, NY, USA, 2010. Dette papir diskuterer generaliserede forestillinger om kontrakt og substituerbarhed .

eksterne links