Alloy & Alloy Analyzer
Rohit Gheyi
[email protected]
Roteiro
1.
2.
3.
4.
5.
6.
7.
Definição e Características
Noções Básicas
A linguagem
O Alloy Analyzer
Exemplo
Comparações com UML/OCL
Conclusões e Bibliografia
1. Definição e Características
Objetivo
Essa apresentação é sobre como
construir e analisar modelos
utilizando a linguagem Alloy
Porque Alloy?
Porque surgiu uma nova linguagem se
já existem muitas outras linguagens e
abordagens para modelar software?
Características
Características dos modelos de Alloy
Micro modelos
Analisável
Declarativa
Estruturada
Micro Modelos
Com poucas linhas dá para se analisar
implementações que possuem milhares
de linhas de código
É uma linguagem pequena e simples
mas é poderosa e flexível o suficiente
para representar sistemas complexos
Analisável
Existe um analisador que simula modelos e
checa suas propriedades
A análise tende não só a fazermos modelos
mais corretos mas também mais sucintos
Não se precisa dar entradas ou casos de
teste ao analisador
Dá para encontrar bugs mais rapidamente
sem muito custo
Declarativa
Um modelo declarativo descreve um estado
de um sistema listando suas propriedades e
restrições
Não especifica como estados são construídos ou
como sua execução leva de um estado para outro
(não indica como uma operação deve ser feita)
E sim, como o estado novo se relaciona com o
estado antigo (reconhece como uma operação
ocorreu)
Estruturada
Sistemas de software possuem pelo menos
dois tipos de complexidade
devido ao event sequencing
devido à estruturação do estado
Alloy foi feito para a tratar a complexidade
estrutural do estado
Existem muitas ferramentas para analisar
seqüências de eventos entretanto poucas
delas analisam estruturas
Mas isso não já existe?
Nem todas as características são
novas
Especificações formais em Z são
declarativas e estruturadas
Linguagens de checagem de modelos
como SMV e Promela são analisáveis
Então, porque Alloy?
Por muito tempo acreditou-se que um
modelo não podia ser declarativo e
analisável ao mesmo tempo
A novidade de Alloy é a combinação
dos quatro itens a modelagem
principalmente
declarativa e analisável (executável)
2. Noções Básicas
Estruturas em Alloy
As estruturas em Alloy são
construídas através de átomos e
relações
Átomos
É uma entidade primária que possui as
seguintes características: indivisível,
imutável, sem interpretação
Relações
É uma estrutura que relaciona átomos
Em Alloy são:
sempre de 1a ordem
sempre finitas
são tipadas
Conjuntos e escalares
Toda expressão é uma relação
Não existem conjuntos
São representados por relações unárias
Não existem escalares
São relações unárias Singletons:
a  {(a)}
Faz a semântica da linguagem ficar simples
e uniforme
Na prática, não precisamos pensar que
conjuntos são relações unárias
Operações sobre Conjuntos
Subconjunto (in)
A in B
União ()
A+B
Interseção ()
A&B
Diferença (-)
A–B
Tamanho do Conjunto (#)
#A
Operadores Relacionais
Transposta (~r)
É a relação inversa
José
pai
~pai=filho
João
João.pai = José
José.~pai = João
Operadores Relacionais
Transitive Closure (^r)
É a união da aplicação da relação r, 1 ou
mais vezes
Exemplo: Ancestrais de jose
jose.^pais = jose.pais + jose.pais.pais +
jose.pais.pais.pais + …
Operadores Relacionais
Join ou Composição
(s1,…,sn-1, sn)
(t1,t2,…, tm)
Join = (s1,…, sn-1, t2,…, tm) , onde sn = t1
Exemplo: Se S for um conjunto e r
uma relação binária:
S.r = é a imagem relacional de S em r
Exemplos
Seja Rohit um escalar, Homem,
Mulher e Pessoa conjuntos e pais e
filhos duas relações binárias:
Rohit.pais
Significado: Quais são os pais de Rohit?
Rohit.pais.~pais = Rohit.pais.filhos
Significado: Quais são os filhos dos pais
de Rohit?
Operadores Lógicos
Conjunção
A && B (A and B)
Disjunção
A || B (A or B)
Negação
! A ou not A
Quantificadores
Seja e é uma expressão:
all - todos ()
all x: e | Fórmula
no – nenhum
no x: e | Fórmula
some – existe ()
some x: e | Fórmula
Exemplos
Toda pessoa, exceto Adao e Eva,
possui uma mãe
all p: Pessoa-Adao-Eva | one p.mae
Existe um homem que é ancestral de
todo mundo, exceto Adao e Eva
some x: Homem | all p: Pessoa-Adao-Eva
| x in p.*(pai+mae)
Observação Importante
Não se pode casar com um irmão
no x: Pessoa | x.esposa in x.irmaos
E se uma pessoa não tiver casada, este fato
é verdadeiro?
Estamos tratando com conjuntos =>
x.esposa = 
 é subconjunto de todo conjunto, inclusive
de x.irmaos
Como achamos uma pessoa, logo o fato não
é verdadeiro
Solução
no x: Pessoa | some(x.esposa) =>
x.esposa in x.irmaos
Tomar cuidado com o conjunto vazio
em Alloy
3. A linguagem
Estrutura de um Programa
1 pacote (module)
0 ou n imports (open/uses)
0 ou n parágrafos
Assinatura (signature)
Fato (fact)
Asserção (assertion)
Função (function)
Rodar (run)
Checar (check)
Avaliar (eval)
Assinatura
Declara um novo tipo e um novo conjunto
A assinatura cria um namespace local
Exemplo:
sig Pessoa {
mae: option Mulher,
pai: option Homem
}
mae é uma relação do tipo: Pessoa  Mulher
Extensão da Assinatura
Não introduz um novo tipo
É um subconjunto da classe pai
Possui o mesmo tipo da classe pai
sig Homem extends Pessoa {
esposa : option Mulher
}
Todos os campos declaradas na classe filha,
são também declaradas na classe pai, só
que sempre retornam .
Fato Implícito: (Pessoa-Homem).esposa = 
Qualificadores
static disj sig Adao, Eva extends
Pessoa { }
static – indica que o Adao e Eva só
possuem 1 átomo (Singleton)
disj – indica que os subconjuntos são
disjuntos. Ou seja: Adao  Eva = 
Relações
sig Pessoa {
mae: option Mulher,
pai: option Homem
}
Seja o átomo p do tipo Pessoa. A relação
mae pode ser chamado das seguintes
formas: (ordem decrescente de precedência)
p::mae
p.mae
mae[p]
Fatos
Fato é uma fórmula que restringe os
valores dos conjuntos e das relações
Exemplo:
fact {all p:Adao+Eva | no (p.pai+p.mae)}
Todas as pessoas p dos conjuntos Adao e
Eva não possuem pais
Fatos Attached
sig Pessoa {
mae: option Mulher,
pai: option Homem
}{
one mae -- significa que toda pessoa tem
}
-- uma mãe
Possui o fato implícito:
all this: Pessoa | with this | one mae
Funções
É uma fórmula parametrizável que
será usada em algum momento.
fun Pessoa::getFilhos(): set Pessoa{
result = this.~pai+ this.~mae
}
Retorna os filhos de uma pessoa
Imports e Pacotes
O pacote é declarado no início do programa
com module:
module library/Lista
sig Lista { fun adicionar() {…} }
Imports devem ser colocados depois do
pacote
Ao importarmos um pacote importamos
também seus fatos
O import em Alloy pode ser feito de 2
formas:
Imports
1. open
Não precisa colocar o nome qualificado
open library/Lista
Ex: adicionar (…)
2. uses
Precisa colocar o nome qualificado
uses library/Lista
Ex: library/Lista/adicionar(…)
4. O Alloy Analyzer
Alloy Analyzer
É uma ferramenta para análise
automática de modelos
É mais um model finder do que um model
checker
É mais um refutador do que um provador
de teoremas
Se ele achar um contra-exemplo ele mostra.
Mas se não mostrar não há garantia de que o
teorema é válido
Asserções
Especifica uma fórmula que é
supostamente verdadeira (teorema).
assert assercaoBiologica {
no p: Pessoa | p in p.^(pai+mae)
}
Ninguém pode ser o seu próprio
ancestral
Comandos
check
Checa se uma asserção é valida. O
resultado dele é um contra-exemplo,
caso exista.
run
É usado para achar uma especificação
válida para uma função.
Comandos
Exemplos:
check A for 3
A asserção (A) é checada para todas as
configurações possíveis onde cada tipo básico
é restringido a não ter mais do que 3 átomos
run func for 3 but 2 S, 5 T
Executa a função (func) com no máximo 3
átomos para cada tipo, exceto o tipo S e T
que possuirão no máximo 2 e 5 átomos
respectivamente
Alloy Analyzer
Painel com
a Sintaxe
(Fórmulas)
Painel da Solução
Painel de Edição
Barra de Status
Visualizador de Soluções
5. Exemplo
Exemplo
module modelos/Pessoa // Pacote
sig Pessoa {
mae: option Mulher,
pai: option Homem
}
disj sig Homem, Mulher extends Pessoa {}
static disj sig Adao extends Homem{}
static disj sig Eva extends Mulher{}
Exemplo
fun Pessoa::getFilhos(): set Pessoa{
result = this.~pai+ this.~mae
}
fact P {
all p:Adao+Eva | no (p.pai+p.mae)
all p: (Pessoa-Adao-Eva) |
one p.pai && one p.mae
all p: Pessoa | all filhos: p..getFilhos() |
filhos ! in (p.^(pai + mae))
}
6. Comparações com
UML/OCL
Relacionamento entre Alloy e
UML
Alloy é similar a OCL mas
possui sintaxe mais convencional
possui semântica mais simples
possibilita análise automática dos modelos
Alloy é uma linguagem totalmente
declarativa
OCL mistura elementos operacionais e
declarativos
Relacionamento entre Alloy e
UML
A utilização do operador ponto (.) em
Alloy dá uma interpretação mais
uniforme e flexível do que OCL
Como os operadores podem ser
aplicados a conjuntos e relações, Alloy
tende a ser mais sucinto do que OCL
Os modelos de OCL são mais difíceis
de ler e escrever
Relacionamento entre Alloy e
UML
Alloy lida com relações com qualquer
aridade
Alloy possui um mecanismo de estruturação
que permite o reuso de fragmentos do
modelo
O modelo em Alloy não só descreve seus
objetos e operações mas também as
propriedades que necessitem serem
checadas
Fato Simples
Fato: O nome de uma criança ou de um amigo não
pode ser dado a nenhum cachorro
OCL:
Person self.pets -> select (d | d.oclKindOf(Dog)) > forall(d | not (self.children ->
union(self.friends) -> collect(q | q.name)) ->
includes(d.name)
Alloy:
all p: Person | all d: p.pets & Dog |
d.name ! in (p.children+p.friends).name
7. Conclusões e Bibliografia
Conclusões
Os pontos fortes dos modelos de
Alloy são:
Micro modelos
Analisável
Estruturada
Declarativa
Alloy possui uma semântica simples e
uniforme
Bibliografia
Artigos, ferramentas, exemplos:
http://sdg.lcs.mit.edu/alloy/
Daniel Jackson – criador do Alloy
http://sdg.lcs.mit.edu/~dnj/
MIT LCS Software Design Group
http://sdg.lcs.mit.edu/