Szerződéses programozás

A szerződéses programozás ( szerződéses tervezés (DbC), szerződés szerinti programozás , szerződésalapú programozás ) egy szoftvertervezési módszer . Azt sugallja, hogy a tervezőnek formális , pontos és ellenőrizhető interfész specifikációkat kell meghatároznia a rendszerkomponensekhez. Ebben az esetben az absztrakt adattípusok szokásos definíciója mellett előfeltételek , utófeltételek és invariánsok is használatosak . Ezeket a specifikációkat "szerződéseknek" nevezik a polgári jogi szerződésekben szereplő feltételek és felelősség fogalmi metaforájának megfelelően .

Történelem

A kifejezést Bertrand Meyer javasolta az Eiffel -nyelv fejlődésével kapcsolatban . A szerződéses programozás formális ellenőrzésből , formális specifikációból és Hoare logikájából nőtt ki . A szerződéses programozás nem csupán egy egyszerű metafora az út megtervezéséhez. A szerződéses programozás használatát megkönnyítő feltételek:

• az öröklődés jelenléte és a dinamikus összekapcsolás lehetősége ,
• a kivételek kezelésének képessége ,
• Automatikus szoftverdokumentáció lehetősége .

Leírás

A szerződéses programozás fő gondolata egy szoftverrendszer elemei közötti interakció modellje, amely a kölcsönös kötelezettségek és előnyök elgondolásán alapul . Az üzleti élethez hasonlóan a vevő és a szállító egy meghatározott szerződés alapján működik . Egyes módszerek vagy funkciók szerződése tartalmazhatja:

• konkrét kötelezettségek, amelyeket bármely ügyfélmodulnak teljesítenie kell a metódus meghívása előtt - előfeltételek , amelyek előnyt jelentenek a szolgáltatónak - nem ellenőrizheti az előfeltételek teljesülését;
• konkrét tulajdonságok, amelyeknek jelen kell lenniük a módszer végrehajtása után - utófeltételek , amelyek a szolgáltató kötelezettségei közé tartoznak;
• meghatározott tulajdonságok teljesítésére vonatkozó kötelezettségek - invariánsok, amelyeket akkor kell teljesíteni, amikor az üzenetszolgáltató megkapja az üzenetet, valamint a metódus kilépésekor.

Sok programozási nyelv lehetővé teszi az ilyen kötelezettségek figyelembevételét. A szerződéses programozás azt jelenti, hogy ezek a követelmények kritikusak a programok helyessége szempontjából, ezért a tervezés során jóvá kell hagyni őket. Így a szerződéses programozás előírja, hogy a kódírást formális helyességi állítások (állítások) megírásával kezdjük.

Az objektumorientált programozásban a metódusszerződés általában a következő információkat tartalmazza:

• lehetséges bemeneti adattípusok és jelentésük;
• visszatérési adattípusok és jelentésük;
• a kivételek előfordulásának feltételei , típusai és értékei;
• a módszer mellékhatásainak jelenléte ;
• az alosztályokban gyengíthető (de nem erősíthető) előfeltételek;
• utófeltételek, amelyek az alosztályokban erősíthetők (de nem gyengíthetők);
• az alosztályokban erősíthető (de nem gyengíthető) invariánsok;
• (néha) teljesítménygaranciák, például időbonyolultság vagy memóriabonyolultság .

Szerződések használatakor magának a kódnak nincs szükség a végrehajtásuk ellenőrzésére. Általában ilyen esetekben kemény esés történik a kódban[ clarify ] (" fail-fast "), így könnyebbé válik a szerződések végrehajtásának hibakeresése. Számos nyelven, például C , C++ , Delphi , PHP , ezt a viselkedést a assert. A kód végső verziójában ez a viselkedés megmarad, vagy az ellenőrzések eltávolíthatók a teljesítmény javítása érdekében.

Az egységtesztek egy modult elkülönítve tesztelnek, ellenőrizve, hogy a modul megfelel-e a szerződésben foglalt feltételezéseknek, és az általa használt modulok teljesítik-e a szerződéseiket. Az integrációs tesztek igazolják, hogy a modulok megfelelően működnek együtt.

A szerződéses programozás növelheti a kód újrafelhasználását , mivel a modul kötelezettségei egyértelműen dokumentáltak. Általánosságban elmondható, hogy a modulszerződés a szoftverek dokumentálásának módjaként is felfogható .

Megvalósítás programozási nyelveken

DbC támogatás nyelvi szinten

A szerződéses programozási eszközöket natívan támogató nyelvek:

• Aktív Oberon
• Ada 2012
• Clojure
• Kobra
• Pascal komponens
• D [1]
• eiffel
• Erőd
• Kotlin
• Lisaac
• Modula-2
• Modula-3
• szép
• Oberon-2
• Oberon-07/11
• Oxigén (korábban Chrome)
• ütő
• Sather
• Scala [2]
• A SPARK az Ada programok statikus elemzésével
• Spec#
• SeC ( C nyelvi kiterjesztés )
• J@va  (lefelé irányuló kapcsolat) ( Java nyelvi kiterjesztés )
• C# (a .NET Framework 4.0 óta)
• Zonnon

DbC támogatás harmadik féltől származó könyvtárakkal

• C és C++ a CTESK -n keresztül , a Contract++ könyvtáron , a DBC for C előfeldolgozóján , a GNU Nana -n vagy a Digital Mars C++ fordítóján keresztül .
• C# kódszerződéseken keresztül
• Menj a dbc -n keresztül
• Java a JavaTESK , iContract2 , Contract4J , jContractor , Jcontract , C4J , CodePro Analytix , STclass , Jass előfeldolgozó, OVal AspectJ segítségével, Java Modeling Language (JML), SpringContracts for Spring Framework vagy Modern Jass , Custos segítségével , vagy Modern Jass , Custos segítségével  (nem elérhető AspectJ hivatkozás használatával ) JavaDbC az AspectJ, cofoja használatával (a Google által kifejlesztett [3] ).
• JavaScript a Cerny.js -n keresztül Archiválva 2007. június 27-én a Wayback Machine -nél , dbc-code-contracts vagy ecmaDebug .
• Selypít
  • Közös Lisp makrókat vagy a CLOS metaobjektum protokollt használva .
  • Séma a PLT kiterjesztésével, nevezetesen az a tény, hogy minden szerződésszegésnek a tettesre kell mutatnia, és pontos magyarázattal kell rendelkeznie. [egy]
• Nemerle makróval.
• Perl a Class::Contract (Damian Conway) vagy a Carp::Datum (Raphael Manfredi) CPAN modulokkal.
• PHP és PhpDeal
• Python a zope.interface csomag, a PyDBC, a PyContracts vagy a Contracts for Python használatával.
• Ruby DesignByContract-el (Brian McCallister), Ruby DBC vagy ruby-contract.
• Rozsda a Hoare könyvtárral [4]
• Vala GLib -el

Általános eszközök

• A Perfect Developer a Perfect specifikációs nyelven keresztül statikus kódelemzés segítségével ellenőrizheti a szerződést, és programokat generálhat olyan nyelveken, mint a C++ és a Java .

Jegyzetek

1. ↑ Walter, Bright D programozási nyelv, szerződéses programozás . Digitális Mars (2014. november 1.). Hozzáférés dátuma: 2014. december 1. Az eredetiből archiválva : 2014. november 28. (határozatlan)
2. ↑ Scala Standard Library Docs - Assertions . EPFL. Letöltve: 2020. január 12. Az eredetiből archiválva : 2019. december 25. (határozatlan)
3. ↑ David Morgan, Andreas Leitner és Nhat Minh Le. Contracts for Java (angol) (2011. február 4.). Letöltve: 2011. június 12. Az eredetiből archiválva : 2012. március 21..  
4. ↑ GitHub - nrc/libhoare: Tervezés a szerződéses stílus kijelentései alapján a Rust számára . Letöltve: 2019. február 24. Az eredetiből archiválva : 2018. október 12.. (határozatlan)

Lásd még

• Modell alapú tesztelés