Wstęp
Programowanie kontraktowe (Design by Contract, DbC) to podejście do projektowania i tworzenia oprogramowania, które polega na formalnym definiowaniu zasad interakcji między komponentami systemu. Wprowadza kontrakty (specyfikacje), które opisują warunki wstępne (preconditions), warunki końcowe (postconditions) oraz niezmienniki (invariants). Dzięki DbC można znacząco poprawić niezawodność i czytelność kodu.
Język Scala, łącząc cechy obiektowego i funkcyjnego programowania, doskonale nadaje się do implementacji konceptu programowania kontraktowego. W tym artykule omówimy, jak można realizować tę technikę natywnie w Scali oraz przedstawimy kilka bibliotek wspierających DbC.
Programowanie kontraktowe w Scali – podejście natywne
Scala, mimo że nie oferuje natywnego wsparcia dla programowania kontraktowego w stylu obecnym w językach takich jak Eiffel, daje elastyczne mechanizmy pozwalające na implementację DbC. Oto kilka sposobów:
1. Używanie asercji
Asercje są najprostszym sposobem realizacji kontraktów. Można je używać do definiowania warunków wstępnych, warunków końcowych i niezmienników.
Przykład kodu divide:
def divide(a: Int, b: Int): Int = {
require(b != 0, "Dzielenie przez zero jest niedozwolone") // Warunek wstępny
val result = a / b
assert(result * b == a, "Niepoprawny wynik dzielenia") // Warunek końcowy
result
}
### wariant drugi kodu
def divide(x: Int, y: Int): Int = {
require(x > y, s"$x > $y")
require(y > 0, s"$y > 0")
x / y
} ensuring (_ * y == x)
Przykład kodu subtract:
def subtract(i: Int, j: Int): Int = {
require(i > 4 && j > 4)
(i - j).ensuring(_ > 4)
}
Przykład kodu subtract:
def subtract(i: Int, j: Int): Int = {
require(i > 4 && j > 4)
(i - j).ensuring(_ > 4)
}
2. Użycie Option lub Either
Scala posiada wbudowane typy takie jak Option czy Either, które umożliwiają obsługę błędów w bardziej deklaratywny sposób.
Przykład z użyciem Either:
def divide(a: Int, b: Int): Either[String, Int] = {
if (b == 0) Left("Dzielenie przez zero jest niedozwolone")
else Right(a / b)
}
3. Nieznaczne wsparcie dla niezmienników w klasach
Przy projektowaniu klas, można wprowadzać sprawdzanie niezmienników przy tworzeniu obiektów.
Przykład:
case class Rectangle(width: Int, height: Int) {
require(width > 0 && height > 0, "Szerokość i wysokość muszą być dodatnie") // Niezmiennik
}
4. Adnotacje i makra
Scala pozwala na definiowanie własnych adnotacji oraz użycie makr do weryfikacji kontraktów w czasie kompilacji.
Adnotacje i makra to potężne narzędzia w języku Scala, które mogą być wykorzystane do implementacji programowania kontraktowego (Design by Contract). Poniżej rozwijam ten temat, aby pokazać, jak te mechanizmy mogą być używane w praktyce.
Adnotacje
Adnotacje w Scali to metadane, które można przypisać do klas, metod, pól, itp. Są wykorzystywane głównie do oznaczania elementów kodu w celu dalszego przetwarzania, np. przez frameworki lub narzędzia do analizy. Możemy jednak używać adnotacji do definiowania kontraktów.
Przykład adnotacji do kontraktów:
Załóżmy, że chcemy stworzyć adnotację @Precondition dla warunków wstępnych i @Postcondition dla warunków końcowych.
import scala.annotation.StaticAnnotation
class Precondition(msg: String) extends StaticAnnotation
class Postcondition(msg: String) extends StaticAnnotation
class Calculator {
@Precondition("b cannot be zero")
@Postcondition("result * b == a")
def divide(a: Int, b: Int): Int = a / b
}
Choć same adnotacje nie weryfikują warunków, mogą być użyte w połączeniu z makrami lub bibliotekami, aby automatycznie sprawdzać kontrakty w czasie kompilacji lub wykonania.
Makra
Makra w Scali umożliwiają wykonywanie kodu w czasie kompilacji, co pozwala na manipulowanie i analizowanie drzewa składniowego programu. Dzięki temu można implementować zaawansowane mechanizmy, takie jak sprawdzanie kontraktów, jeszcze zanim kod zostanie uruchomiony.
Przykład użycia makr do weryfikacji kontraktów:
Makra mogą przetwarzać adnotacje, aby dodać sprawdzanie warunków bezpośrednio do generowanego kodu. Poniżej uproszczony przykład makra, które sprawdza warunki wstępne.
import scala.language.experimental.macros
import scala.reflect.macros.blackbox
object ContractMacros {
def precondition(condition: Boolean, msg: String): Unit = macro preconditionImpl
def preconditionImpl(c: blackbox.Context)(condition: c.Expr[Boolean], msg: c.Expr[String]): c.Expr[Unit] = {
import c.universe._
condition.tree match {
case Literal(Constant(true)) => reify(())
case _ => reify {
if (!condition.splice) throw new IllegalArgumentException(msg.splice)
}
}
}
}
object Example {
import ContractMacros._
def divide(a: Int, b: Int): Int = {
precondition(b != 0, "b cannot be zero")
a / b
}
}
W tym przykładzie funkcja precondition jest makrem, które weryfikuje warunek wstępny w czasie kompilacji lub dodaje odpowiedni kod do sprawdzania w czasie wykonania.
Zalety podejścia z adnotacjami i makrami
- Automatyzacja: Makra mogą generować kod sprawdzający kontrakty, co zmniejsza ryzyko błędów i ułatwia utrzymanie kodu.
- Wydajność: Dzięki makrom warunki mogą być weryfikowane w czasie kompilacji, co redukuje narzut w czasie wykonania.
- Czytelność: Adnotacje jasno komunikują intencje programisty, zwiększając czytelność kodu.
Biblioteki wspierające Design by Contract w Scali
Podczas gdy podejście natywne jest wystarczające dla prostych projektów, bardziej zaawansowane zastosowania mogą skorzystać z bibliotek wspierających programowanie kontraktowe. Oto kilka z nich:
1. Strong type constraints for Scala
Iron to biblioteka wprowadzająca programowanie kontraktowe w Scali na zasadzie silnego typowania. Pozwala na definiowanie silnych i bardzo skonkretyzowanych typów. Warto zaznaczyć, że to nie są czyste kontrakty w koncepcie DbC, ale bardzo dobrze wiedzieć, że silne typy stanowią podstawę poprawności kodu.
Przykład użycia:
import io.github.iltotore.iron.*
import io.github.iltotore.iron.constraint.numeric.*
def log(x: Double :| Positive): Double =
Math.log(x) //Used like a normal `Double`
log(1.0) // automatyczna weryfikacja w czasie kompilacji
log(-1.0) // Błąd w czasie kompulacji: Wartość powinna być pozytywnym typem Double - podano ujemną wartość!
### wyjście na STDOUT
-- Constraint Error --------------------------------------------------------
Could not satisfy a constraint for type scala.Double.
Value: -1.0
Message: Should be strictly positive
----------------------------------------------------------------------------
2. ScalaCheck
Choć ScalaCheck jest bardziej narzędziem do testowania, pozwala na weryfikację właściwości (ang. property-based testing), co jest związane z ideą niezmienników.
Przykład:
import org.scalacheck.Properties
import org.scalacheck.Prop.forAll
object DivisionSpec extends Properties("Division") {
property("Divide") = forAll { (a: Int, b: Int) =>
(b != 0) ==> ((a / b) * b == a)
}
}
3. Cats
Biblioteka Cats + Validated oferuje zaawansowane struktury danych i funkcje umożliwiające bardziej deklaratywne podejście do programowania kontraktowego.
Przykład z użyciem Validated:
import cats.data.Validated
import cats.implicits._
def divide(a: Int, b: Int): Validated[String, Int] =
if (b == 0) "Dzielenie przez zero jest niedozwolone".invalid
else (a / b).valid
4. Stainless
Stainless to zaawansowane narzędzie do weryfikacji formalnej programów napisanych w języku Scala. Jest rozwijane przez Laboratorium Automatyzacji i Analizy Formalnej (LARA) na Politechnice Federalnej w Lozannie (EPFL). Stainless pozwala na analizę i dowodzenie właściwości programów, takich jak bezpieczeństwo typów, niezmienniki, czy poprawność funkcji, przy użyciu technik formalnych.
Główne cechy Stainless
- Weryfikacja właściwości: Stainless umożliwia dowodzenie poprawności kodu na podstawie specyfikacji, takich jak warunki wstępne, warunki końcowe i niezmienniki.
- Wsparcie dla Scali: Narzędzie obsługuje podzbiór języka Scala, w tym funkcje wyższego rzędu, rekurencję, typy algebraiczne (ADT) i niezmienniki.
- Integracja z SMT Solverami: Stainless wykorzystuje SMT Solvery (np. Z3) do automatycznego dowodzenia właściwości programów.
- Wsparcie dla Scali 3: Stainless jest kompatybilny z najnowszymi wersjami Scali, co czyni go aktualnym i użytecznym narzędziem.
Przykład użycia Stainless
Poniżej znajduje się przykład programu, który definiuje funkcję myTail z warunkiem wstępnym, że lista wejściowa nie może być pusta:
import stainless.collection._ object HelloStainless { def myTail(xs: List[BigInt]): BigInt = { require(xs.nonEmpty, „Lista nie może być pusta”) // Warunek wstępny xs match { case Cons(h, _) => h // Dopasowanie jest wyczerpujące } } }
5. Scaladbc
Biblioteka scaladbc to projekt dostępny na GitHubie, który wspiera programowanie kontraktowe (Design by Contract) w języku Scala. Projekt umożliwia definiowanie kontraktów, takich jak warunki wstępne, warunki końcowe i niezmienniki, w sposób czytelny i zintegrowany z kodem.
Przykład użycia scaladbc:
scala
import scaladbc._
def divide(a: Int, b: Int): Int = dbc {
pre(b != 0, "Dzielenie przez zero jest niedozwolone")
post(result => result * b == a, "Wynik dzielenia jest niepoprawny")
body(a / b)
}Podsumowanie
Programowanie kontraktowe to potężne narzędzie, które zwiększa jakość i niezawodność kodu. Scala, dzięki swojej elastyczności, umożliwia natywną implementację DbC, oferując również możliwość skorzystania z zaawansowanych bibliotek. Korzystając z tych narzędzi, programiści mogą skutecznie projektować, implementować i weryfikować kontrakty w aplikacjach.
Zachęcamy do eksperymentowania z DbC w Scali, ponieważ poprawa jakości kodu to inwestycja, która procentuje w każdym projekcie!
