Specyfikacja algebraiczna
Specyfikacja algebraiczna to technika inżynierii oprogramowania służąca do formalnego określania zachowania systemu. Był to bardzo aktywny przedmiot badań informatycznych około 1980 roku.
Przegląd
Specyfikacja algebraiczna ma na celu systematyczne rozwijanie bardziej wydajnych programów poprzez:
- formalne definiowanie typów danych i operacje matematyczne na tych typach danych
- abstrahowanie szczegółów implementacji, takich jak rozmiar reprezentacji (w pamięci) i efektywność uzyskiwania wyników obliczeń
- sformalizowanie obliczeń i operacji na typach danych
- umożliwienie automatyzacji poprzez formalne ograniczenie operacji do tego ograniczonego zestawu zachowań i typów danych.
Specyfikacja algebraiczna osiąga te cele, definiując jeden lub więcej typów danych i określając zbiór funkcji, które działają na tych typach danych. Funkcje te można podzielić na dwie klasy:
- Funkcje konstruktora : funkcje, które tworzą lub inicjują elementy danych lub konstruują złożone elementy z prostszych. Zestaw dostępnych funkcji konstruktora jest implikowany przez sygnaturę specyfikacji . Dodatkowo specyfikacja może zawierać równania określające równoważności między obiektami konstruowanymi przez te funkcje. To, czy podstawowa reprezentacja jest identyczna dla różnych, ale równoważnych konstrukcji, zależy od implementacji.
- Funkcje dodatkowe : Funkcje, które działają na typach danych i są zdefiniowane w kategoriach funkcji konstruktora.
Przykłady
Rozważmy formalną specyfikację algebraiczną dla typu danych boolowskich .
Jedna możliwa specyfikacja algebraiczna może zapewniać dwie funkcje konstruktora dla elementu danych: prawdziwy konstruktor i fałszywy konstruktor. W ten sposób boolowski element danych może zostać zadeklarowany, skonstruowany i zainicjowany do wartości. W tym scenariuszu wszystkie inne elementy łączące , takie jak XOR i AND , byłyby funkcjami dodatkowymi . W ten sposób element danych może zostać utworzony z wartością „prawda” lub „fałsz”, a dodatkowe funkcje mogą zostać użyte do wykonania dowolnej operacji na elemencie danych.
Alternatywnie cały system boolowskich typów danych można określić za pomocą innego zestawu funkcji konstruktora: fałszywego konstruktora i niekonstruktora . W takim przypadku można zdefiniować dodatkową funkcję true , aby uzyskać wartość not false i równanie należy dodać.
Specyfikacja algebraiczna opisuje zatem wszystkie możliwe stany elementu danych i wszystkie możliwe przejścia między stanami. [ potrzebne źródło ]
W przypadku bardziej skomplikowanego przykładu liczby całkowite można określić (wśród wielu innych sposobów i wybierając jeden z wielu formalizmów) za pomocą dwóch konstruktorów
1 : Z (_ - _): Z × Z -> Z
i trzy równania:
(1 - (1 - p)) = p ((1 - (n - p)) - 1) = (p - n) ((p1 - n1) - (n2 - p2)) = (p1 - (n1 - (p2 - n2)))
Łatwo jest sprawdzić, czy równania są poprawne, biorąc pod uwagę zwykłą interpretację binarnej funkcji „minus”. (Nazwy zmiennych zostały wybrane tak, aby wskazywały na dodatnie i ujemne wkłady w wartość). Niewielkim wysiłkiem można wykazać, że zastosowane od lewej do prawej tworzą one również zlewający się i kończący system przepisywania, odwzorowujący dowolny skonstruowany termin na jednoznaczna postać normalna reprezentująca odpowiednią liczbę całkowitą:
... (((1 - 1) - 1) - 1) ((1 - 1) - 1) (1 - 1) 1 (1 - ((1 - 1) - 1)) (1 - ((( 1 - 1) - 1) - 1)) ...
Dlatego każda implementacja zgodna z tą specyfikacją będzie zachowywać się jak liczby całkowite lub ewentualnie ich ograniczony zakres , jak zwykłe typy liczb całkowitych występujące w większości języków programowania.