Alloy
specyfikacja: zbiór formuł, które określają zakładane okoliczności użycia software'u
model: zbiór z działaniami spełniający specyfikację
czy istnieje model specyfikacji? — niesprzeczność / czy dla każdego modelu specyfikacji zachodzi pewna własność?
Alloy — system wspomagający modelowanie software'u opracowany w MIT
może generować przykłady / kontrprzykłady specyfikacji
założenie pragmatyczne: jeśli coś jest źle, mały kontrprzykład to pokaże
Instalacja Alloy
należy pobrać plik wykonywalny Javy dostępny na GitHubie alloy6.2.jar lub wersję lokalną
i wywołać
java -jar org.alloytools.alloy.dist.jar
wcześniejsze wersje na stronie producenta: download.html
(alloy5.jar lub lokalnie czy nawet alloy4.2.jar, lokalnie)
Praca z Alloy
w oknie edycyjnym należy wpisywać fragmenty specyfikacji wraz z poleceniami
run .... check ...
generującymi przykład modelu lub sprawdzające, że nie ma konktrprzykładu
a następnie należy wykonywać w/w polecenia i oglądać wyniki w wersji graficznej
po czym następuje powrót do edycji specyfikacji
Dokumentacja Alloy
nowa wersja: Practical Alloy
dokumentacja (z wyjątkiem książki)
książka: Software Abstractions
materiały, na których oparto część wykładu
tutorial online dla v.4.