Programování smluv

Smluvní programování ( design by contract (DbC), programování na základě smlouvy , programování založené na smlouvě ) je metoda návrhu softwaru . Navrhuje, že návrhář musí definovat formální , přesné a ověřitelné specifikace rozhraní pro systémové komponenty. V tomto případě se kromě obvyklé definice abstraktních datových typů používají také předpoklady , postpodmínky a invarianty . Tyto specifikace se nazývají „smlouvy“ v souladu s konceptuální metaforou podmínek a odpovědností v občanskoprávních smlouvách .

Historie

Termín navrhl Bertrand Meyer v souvislosti s vývojem Eiffelova jazyka . Smluvní programování vyrostlo z formálního ověření , formální specifikace a Hoareovy logiky . Smluvní programování není jen jednoduchou metaforou pro navrhování způsobu. Podmínky, které usnadňují používání smluvního programování:

• přítomnost dědičnosti a možnost dynamického propojení ,
• schopnost zvládat výjimky ,
• Možnost automatické softwarové dokumentace .

Popis

Hlavní myšlenkou smluvního programování je model interakce mezi prvky softwarového systému založený na myšlence vzájemných závazků a výhod . Stejně jako v podnikání, zákazník a dodavatel fungují na základě konkrétní smlouvy . Smlouva o nějaké metodě nebo funkci může zahrnovat:

• konkrétní povinnosti, které musí splnit kterýkoli klientský modul před voláním metody - předpoklady , které zvýhodňují poskytovatele - nesmí kontrolovat splnění podmínek;
• specifické vlastnosti, které musí být přítomny po provedení metody - postconditions , které jsou zahrnuty v povinnostech poskytovatele;
• povinnosti splnit specifické vlastnosti - invarianty, které musí být splněny, když poskytovatel zprávy obdrží zprávu, stejně jako při ukončení metody.

Mnoho programovacích jazyků umožňuje takové povinnosti vzít v úvahu. Smluvní programování znamená, že tyto požadavky jsou kritické pro správnost programů, takže musí být schváleny během návrhu. Smluvní programování tedy předepisuje začít psát kód psaním formálních tvrzení o správnosti (tvrzení).

V objektově orientovaném programování smlouva o metodě obvykle obsahuje následující informace:

• možné typy vstupních dat a jejich význam;
• návratové datové typy a jejich význam;
• podmínky pro vznik výjimek , jejich druhy a hodnoty;
• přítomnost vedlejšího účinku metody;
• předpoklady, které lze v podtřídách oslabit (ale nikoli posílit);
• postpodmínky, které lze v podtřídách posílit (ale nikoli oslabit);
• invarianty, které mohou být zesíleny (ale ne oslabeny) v podtřídách;
• (někdy) záruky výkonu, jako je časová složitost nebo paměťová složitost .

Při používání smluv není vyžadován samotný kód ke kontrole jejich provedení. Obvykle v takových případech je v kódu proveden tvrdý pád[ objasnit ] (" fast-fast "), což usnadňuje ladění provádění smluv. V mnoha jazycích, jako je C , C++ , Delphi , PHP , je toto chování implementováno pomocí assert. V konečné verzi kódu může být toto chování zachováno nebo mohou být kontroly odstraněny, aby se zlepšil výkon.

Unit testy testují modul izolovaně a ověřují, že modul splňuje předpoklady smlouvy a že moduly, které používá, plní své smlouvy. Integrační testy ověřují, že moduly spolupracují správně.

Programování smluv může zvýšit opětovné použití kódu , protože povinnosti modulu jsou jasně zdokumentovány. Obecně lze smlouvu na modul chápat také jako způsob dokumentace softwaru .

Implementace v programovacích jazycích

Podpora DbC na jazykové úrovni

Jazyky nativně podporující smluvní programovací nástroje:

• Aktivní Oberon
• Ada 2012
• Clojure
• Kobra
• Komponenta Pascal
• D [1]
• eiffel
• Pevnost
• Kotlin
• Lisaac
• Modul-2
• Modul-3
• Pěkný
• Oberon-2
• Oberon-07/11
• Oxygene (bývalý Chrome)
• raketa
• Sather
• Scala [2]
• SPARK prostřednictvím statické analýzy programů Ada
• specifikace#
• SeC ( rozšíření jazyka C )
• J@va  (downlink) ( rozšíření jazyka Java )
• C# (od .NET Framework 4.0)
• Zonnon

Podpora DbC s knihovnami třetích stran

• C a C++ přes CTESK , knihovnu Contract++ , preprocesor DBC pro C , GNU Nana nebo kompilátor Digital Mars C++ .
• C# prostřednictvím Code Contracts
• Přejít přes dbc
• Java přes JavaTESK , iContract2, Contract4J , jContractor , Jcontract, C4J , CodePro Analytix, STclass , preprocesor Jass, OVal s AspectJ, Java Modeling Language (JML), SpringContracts pro Spring Framework nebo Modern Jass , Custos  (nedostupný odkaz) pomocí AspectJ JavaDbC pomocí AspectJ, cofoja (vyvinutý [3] společností Google ).
• JavaScript přes Cerny.js Archivováno 27. června 2007 na Wayback Machine , dbc-code-contracts nebo ecmaDebug .
• Lisp
  • Common Lisp pomocí maker nebo protokolu metaobjektů CLOS .
  • Schéma rozšířením PLT, totiž skutečnost, že každé porušení smlouvy musí ukazovat na viníka a mít přesné vysvětlení. [jeden]
• Nemerle s makry.
• Perl pomocí modulů CPAN Class::Contract (Damian Conway) nebo Carp::Datum (Raphael Manfredi).
• PHP s PHPDeal
• Python pomocí balíčku zope.interface, PyDBC, PyContracts nebo Contracts for Python.
• Ruby s DesignByContract (od Briana McCallistera), Ruby DBC nebo ruby-contract.
• Rust s knihovnou Hoare [4]
• Vala s GLib

Obecné nástroje

• Perfect Developer může prostřednictvím jazyka Perfect Specification zkontrolovat smlouvu pomocí statické analýzy kódu a generovat programy v jazycích jako C++ a Java .

Poznámky

1. ↑ Walter, programovací jazyk Bright D, smluvní programování . Digitální Mars (1. listopadu 2014). Datum přístupu: 1. prosince 2014. Archivováno z originálu 28. listopadu 2014. (neurčitý)
2. ↑ Dokumenty standardní knihovny Scala – tvrzení . EPFL. Staženo 12. ledna 2020. Archivováno z originálu 25. prosince 2019. (neurčitý)
3. ↑ David Morgan, Andreas Leitner a Nhat Minh Le. Contracts for Java (anglicky) (4. února 2011). Získáno 12. června 2011. Archivováno z originálu 21. března 2012.  
4. ↑ GitHub - nrc/libhoare: Návrh podle stylu smlouvy pro Rust . Staženo 24. února 2019. Archivováno z originálu 12. října 2018. (neurčitý)

Viz také

• Testování založené na modelu