Background for the header
To the home page of the University of Antwerp

 

 

Design By Contract

Doel

Het doel van deze les is het definieren en werken met design by contract technieken in een programmeertaal (Java).

Design By Contract

De basis van design by contract wordt gevormd door de verifieerbare contracten die in de programma-tekst verweven zitten. Door het gebruik van dergelijke contracten worden de veronderstellingen van de ontwikkelaars expliciet gemaakt waardoor (her)gebruik wordt vereenvoudigd. Vermits vele talen dateren van voor de introductie van design by contract, ontbreekt ingebouwde ondersteuning voor design by contract. Dit houdt niet weg dat vele talen elementen van design by contract hebben ingevoegd zelfs tot in de taal zelf (bv. assert in Java) of via preprocessing technieken (bv. JML).

In dit practicum gaan we gebruik maken van een kleine lightweight library die in house (bij Ansymo zelf) is ontwikkeld. Adbc is een library die design by contract ondersteuning voorziet voor de AspectJ programmeertaal (een uitbreiding van Java die Aspect oriented programming toelaat). Aangezien AspectJ een uitbreiding is van Java, kunnen we deze tool ook gebruiken voor contracten in Java zelf. De tool zelf bestaat in essentie uit een reeks aspecten die at runtime de contracten zal verifieren en een exception gooit indien er een contract verbroken wordt.

In Adbc worden contracten geschreven in Java annotations:

  • @requires Specifies the preconditions of a method or a constructor. This annotation takes one or more strings as its value, where each string is a contract specified as a boolean expression.
  • @ensures Specifies the postconditions of a method or a constructor.
  • @invariant Specifies the invariants of a class.

Bij het schrijven van contracten zijn ook de volgende variabelen en functies beschikbaar:

  • $this The this object.
  • parameters The parameters of methods can be simply accessed using their name.
  • $result The return value of a method, available only in postconditions.
  • $old(expr) The $old function can only be used in postconditions. It evaluates an expression before the method is executed, stores the result, and makes it available in postconditions. This is useful if, for example, you want to compare the old value of a field with its new value.
  • $super When used in a precondition of an overriding method, $super refers to the preconditions of the overridden method. Likewise, when used in the postconditio , $super refers to the postconditions of the overridden method. Used in an invariant, it refers to the invariants of the super class.

Hetvolgende code voorbeeld toont aan de hand van een eenvoudige Square klasse de syntax voor eenvoudige contracten.

Merk op dat een contract uit meerdere delen kan bestaan (een array van strings). Bijvoorbeeld de postconditie van setSize() bestaat uit twee delen: $this.getHeight()==s en $this.getWidth()==s. Dit is het equivalent van $this.getHeight()==s && $this.getWidth()==s. Het voordeel van een contract van een contract op te splitsen in meerdere delen is dat wanneer een contract verbroken is de tool meer specifiek kan zeggen welk deel van het contract verbroken was.

Meer informatie over Adbc kan je vinden in de readme.

Opgave

  • Schrijf de contracten uit voor een kleine kassa toepassing die klanten toelaat hun aankopen uit de winkel af te rekenen. Een meer gedetailleerde beschrijving vind je onderaan. Houd je aan het vooropgestelde ontwerp
  • Implementeer de basis van het systeem
  • Voer het systeem met de contracten uit
  • Doe een analyse van het systeem aan de hand van de contracten

Project Beschrijving

De klant selecteert de gewenste producten. De klant kan altijd producten verwijderen of toevoegen zolang de geselecteerde producten niet volledig afgerekend zijn. De klant geeft zijn aankopen af aan de kassa. Nadien betaalt hij het gewenste bedrag met de betaalmiddelen die hij ter beschikking heeft. Hij kan bv. het bedrag betalen door een deel cash en een deel met proton te betalen. Van zodra het kasbedrag bereikt werd wordt zijn rekening afgedrukt. Op de rekening komen alle items die hij heeft aangekocht. Het ticket vermeldt per product de aard van het product, bij gewogen producten komt daar nog een regel bij die het aangekochte gewicht weergeeft. Het is ook mogelijk een product een korting toe te kennen. De aangeboden korting voor stukartikelen mag nooit groter zijn dan de prijs van het artikel en is zeker meer dan nul euro. Voor gewogen artikelen wordt de korting uitgedrukt in een gewichtcategorie (i.e. veelvoud van 100), maar mag nooit groter zijn dan het gewicht van het product.

Vooropgesteld ontwerp:

Valid HTML 4.01! Valid CSS!

 Lab On REengineering - Antwerpen, last modified 13:23:40 02 November 2014