Kontraktsprogrammering

Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 1 december 2014; kontroller kräver 33 redigeringar .

Kontraktsprogrammering ( design by contract (DbC), programmering genom kontrakt , kontraktsbaserad programmering ) är en mjukvarudesignmetod . Det föreslår att designern måste definiera formella , exakta och verifierbara gränssnittsspecifikationer för systemkomponenter. I det här fallet används förutom den vanliga definitionen av abstrakta datatyper även preconditions , postconditions och invarianter . Dessa specifikationer kallas "kontrakt" i enlighet med den konceptuella metaforen om villkor och ansvar i civilrättsliga avtal .

Historik

Termen föreslogs av Bertrand Meyer i samband med utvecklingen av Eiffelspråket . Kontraktsprogrammering växte fram ur formell verifiering , formell specifikation och Hoares logik . Kontraktsprogrammering är inte bara en enkel metafor för att designa ett sätt. Villkor som underlättar användningen av avtalsprogrammering:

Beskrivning

Huvudidén med kontraktsprogrammering är en modell för interaktion mellan elementen i ett mjukvarusystem baserat på idén om ömsesidiga skyldigheter och fördelar . Som i affärer arbetar kunden och leverantören under ett specifikt avtal . Kontraktet för någon metod eller funktion kan innehålla:

Många programmeringsspråk tillåter att sådana skyldigheter beaktas. Kontraktsprogrammering innebär att dessa krav är avgörande för att programmen är korrekta, så de måste godkännas under utformningen. Kontraktsprogrammering föreskriver alltså att börja skriva kod genom att skriva formella påståenden om riktighet (påståenden).

I objektorienterad programmering innehåller ett metodkontrakt vanligtvis följande information:

Vid användning av kontrakt krävs inte själva koden för att kontrollera deras exekvering. Vanligtvis görs i sådana fall ett hårt fall i koden[ clarify ] (" fail-fast "), vilket gör det lättare att felsöka utförandet av kontrakt. På många språk som C , C++ , Delphi , PHP implementeras detta beteende av assert. I den slutliga versionen av koden kan detta beteende bevaras, eller så kan kontrollerna tas bort för att förbättra prestandan.

Enhetstester testar en modul isolerat och verifierar att modulen uppfyller kontraktets antaganden och att modulerna den använder uppfyller sina kontrakt. Integrationstest verifierar att moduler fungerar korrekt tillsammans.

Kontraktsprogrammering kan öka kodåteranvändningen eftersom modulens skyldigheter är tydligt dokumenterade. Generellt sett kan modulkontraktet också ses som ett sätt att dokumentera programvara .

Implementering i programmeringsspråk

DbC-stöd på språknivå

Språk som stöder kontraktsprogrammeringsverktyg:

DbC-stöd med tredje parts bibliotek

Allmänna verktyg

Anteckningar

  1. Walter, Bright D-programmeringsspråk, kontraktsprogrammering . Digital Mars (1 november 2014). Datum för åtkomst: 1 december 2014. Arkiverad från originalet den 28 november 2014.
  2. Scala Standard Library Docs - Påståenden . EPFL. Hämtad 12 januari 2020. Arkiverad från originalet 25 december 2019.
  3. David Morgan, Andreas Leitner och Nhat Minh Le. Kontrakt för Java (engelska) (4 februari 2011). Hämtad 12 juni 2011. Arkiverad från originalet 21 mars 2012.  
  4. GitHub - nrc/libhoare: Design by contract style assertions for Rust . Hämtad 24 februari 2019. Arkiverad från originalet 12 oktober 2018.

Se även