Stop (język specyfikacji)
W informatyce i inżynierii oprogramowania Alloy jest deklaratywnym językiem specyfikacji służącym do wyrażania złożonych ograniczeń strukturalnych i zachowania w systemie oprogramowania . Alloy zapewnia proste narzędzie do modelowania konstrukcji oparte na logice pierwszego rzędu . Alloy jest ukierunkowany na tworzenie mikromodeli , które następnie mogą być automatycznie sprawdzane pod kątem poprawności . Specyfikacje stopów można sprawdzić za pomocą analizatora stopów.
Chociaż Alloy został zaprojektowany z myślą o automatycznej analizie, Alloy różni się od wielu języków specyfikacji zaprojektowanych do sprawdzania modeli tym, że umożliwia definiowanie nieskończonych modeli. Analizator stopu jest przeznaczony do przeprowadzania kontroli w ograniczonym zakresie, nawet na nieskończonych modelach.
Język i analizator Alloy zostały opracowane przez zespół kierowany przez Daniela Jacksona z Massachusetts Institute of Technology w Stanach Zjednoczonych .
Historia i wpływy
Pierwsza wersja języka Alloy pojawiła się w 1997 roku. Był to raczej ograniczony język modelowania obiektowego . Kolejne iteracje języka „dodały kwantyfikatory , wyższe relacje arity , polimorfizm , podtypy i podpisy”.
Na matematyczne podstawy języka duży wpływ miała notacja Z , a składnia Alloy zawdzięcza więcej językom takim jak Object Constraint Language .
Analizator stopów
Analizator stopu został specjalnie opracowany do obsługi tak zwanych „lekkich metod formalnych”. Jako taki ma na celu zapewnienie w pełni zautomatyzowanej analizy, w przeciwieństwie do interaktywnych technik dowodzenia twierdzeń, powszechnie stosowanych w językach specyfikacji podobnych do Alloy. Rozwój analizatora był pierwotnie inspirowany zautomatyzowaną analizą zapewnianą przez kontrolery modeli . Jednak sprawdzanie modelu nie nadaje się do modeli, które są zwykle opracowywane w programie Alloy, w wyniku czego rdzeń analizatora został ostatecznie zaimplementowany jako wyszukiwarka modeli zbudowana na boolowskim solwerze SAT .
W wersji 3.0 Alloy Analyzer zawierał integralną wyszukiwarkę modeli opartą na SAT, opartą na gotowym rozwiązaniu SAT. Jednak od wersji 4.0 Analyzer wykorzystuje wyszukiwarkę modeli Kodkod, dla której Analyzer działa jako front-end. Oba narzędzia do wyszukiwania modeli zasadniczo tłumaczą model wyrażony w logice relacyjnej na odpowiednią logiczną formułę logiczną, a następnie odwołują się do gotowego rozwiązania SAT dla formuły logicznej. W przypadku, gdy solver znajdzie rozwiązanie, wynik jest ponownie tłumaczony na odpowiednie powiązanie stałych ze zmiennymi w relacyjnym modelu logicznym.
Aby upewnić się, że problem znalezienia modelu jest rozstrzygalny , Alloy Analyzer przeprowadza wyszukiwanie modelu w ograniczonych zakresach składających się ze zdefiniowanej przez użytkownika skończonej liczby obiektów. Powoduje to ograniczenie ogólności wyników uzyskiwanych przez analizator. Jednak projektanci Alloy Analyzer uzasadniają decyzję o pracy w ograniczonych zakresach odwołując się do hipotezy o małym zakresie : że dużą część błędów można znaleźć, testując program dla wszystkich danych wejściowych testu w pewnym małym zakresie.
Struktura modelu
Modele stopowe mają charakter relacyjny i składają się z kilku różnych rodzajów stwierdzeń:
- Sygnatury definiują słownictwo modelu poprzez tworzenie nowych zestawów
-
sig Obiekt{}definiuje sygnaturę Obiekt sig -
List { head : samotny Węzeł }definiuje sygnaturę Lista zawierająca nagłówek pola typu Węzeł i krotność lone - stwierdza istnienie relacji między listami a węzłami w taki sposób, że każda lista jest powiązana z nie więcej niż jednym głównym węzłem
-
- Fakty to ograniczenia, które z założenia zawsze obowiązują
- Predykaty są sparametryzowanymi ograniczeniami i mogą być używane do reprezentowania operacji
- Funkcje to wyrażenia, które zwracają wyniki
- Asercje to założenia dotyczące modelu
Ponieważ Alloy jest językiem deklaratywnym, kolejność instrukcji nie ma wpływu na znaczenie modelu.