Levantando Requisitos e Procurando Bugs a Partir do Design com Alloy Analyzer

Antes da construção de qualquer sistema, é preciso levantar requisitos, observando as possíveis restrições que o domínio possui. Por exemplo, um sistema de apoio a gestão de RH permite a concessão de licença maternidade a gestantes, mas o que acontece se ele conceder a pessoas do sexo masculino? Alguns requisitos e suas restrições parecem óbvios, mas mesmo o que pode parecer evidente pode não ser. Um exemplo simples seria, algo que todos que já se depararam em um curso de programação, o que faz um algoritmo de ordenação? A resposta evidente seria: um algoritmo que possui como saída uma lista ou sequência ordenada. Seria essa a especificação correta? A partir desse exemplo, vamos explorar uma maneira de levantar requisitos a partir do design do algoritmo.

A ferramenta que será utilizada para explorar a busca por especificações será o Alloy Analyzer (https://alloytools.org/). Alloy Analyzer é uma linguagem e analisador open source para modelagem de software. Essa ferramenta foi desenvolvida pelo Software Design Group do MIT. Para analisar as restrições nessas relações, ele funciona tentando resolver quebra-cabeças, com a ajuda de um SMT solver. SMT solvers tentam procurar a resposta da seguinte questão: dada um fórmula escrita em lógica proposicional, qual a instância que deixa a fórmula válida? Alloy, traduz o código fonte do modelo nesse tipo de pergunta. Como para usar um carro, não é necessário saber a forma completa de como ele funciona, mas alguns detalhes, por exemplo, se ele é a diesel ou a gasolina. Assim o que se precisa saber é que, medida que se aumenta um pouco o número de instâncias possíveis para o modelo, o tempo de geração de exemplos e contra-exemplos aumenta muitíssimo. Na verdade, essa é uma restrição da tecnologia dos SMT solvers e quem conseguir resolvê-la ganha um milhão de dólares, pois envolve os problemas NP-Completos (https://en.wikipedia.org/wiki/Millennium_Prize_Problems).

Como linguagem, Alloy funciona descrevendo objetos, assim como na Programação Orientada a Objetos, mas ao invés das classes serem caracterizadas pelos atributos e métodos, as classes são caracterizadas por relações entre seus objetos. Por exemplo (disponível em : https://github.com/thiagomendoncaferreiraramos/Alloy), tem-se o seguinte código:

sig Elem{}

A palavra reservada "sig" indica que o que vem a seguir é uma classe. "Elem" é uma classe e as chaves vazias indicam que a classe não possui relação especificada. Alloy pode gerar alguns exemplos especificados a partir desse modelo. Quando não especificada a quantidade de objetos, Alloy gera até três objetos para cada classe especificada, mas pode ser especificado até mais dependendo da vontade do usuário. Na seguinte figura gerada pela ferramenta, tem-se dois objetos da classe "Elem".

O próximo código a ser escrito, descreve uma relação de ordem entre os objetos e descreve que o modelo pode ter até sete objetos por classe:

sig Elem{
  lessThan: Elem
}


run {} for 7

Dentro das chaves da classe "Elem" foi descrita a relação "lessThan", que relaciona dois objetos da classe "Elem" e representa que um objeto é menor que o outro no sentido de ser um sucessor.

A sentença "run {} for 7" indica que o modelo terá até 7 objetos por classe. Um exemplo gerado seria:

Observa-se que a relação "lessThan" está representando erroneamente que um elemento é menor que ele mesmo. Algo que pode acontecer também é a relação ser "circular". Por exemplo, "A" está relacionado com "B", que está relacionado com "C", que está relacionado com "A". Para evitar essas duas situações, algumas restrições serão acrescentadas ao modelo.

sig Elem{
  lessThan: set Elem
}


fact Injective{
  ~lessThan.lessThan in iden
}


fact Asymmetric{
  no ^lessThan & ~(^lessThan)
}


fact Acyclic{
  (Elem->Elem-iden in ^lessThan + ~(^lessThan))
}


run {} for 7

A palavra reservada "fact" indica algumas restrições no modelo. A primeira restrição diz que a relação "lessThan" é injetiva. Isso significa que um objeto é menor que a no máximo um outro objeto que que este outro objeto é maior que no máximo a um objeto.

Observe o que está escrito dentro das chaves: "~lessThan.lessThan in iden" O ponto "." é o operador de composição de relações. Um exemplo de composição de relações está na figura abaixo:

No exemplo acima, tem-se a relação de do que as pessoas leram e os assuntos do livro. A composição de relações seria o que as pessoas aprenderam. Na relação "~lessThan" o símbolo do til "~" indica o converso de uma relação. Como exemplo de converso, tem-se:

O converso de relação de leitura seria de livros que foram lidos por. Por fim, "Rel in iden" indica que a relação "Rel" está contido na relação identidade, que é a relação de todos os objetos que estão relacionados consigo mesmo.

O segunda restrição diz que o fecho transitivo da relação "lessThan" é assimétrica. Observe o que está escrito dentro das chaves: "no ^lessThan & ~(^lessThan)" O operador de acento circunflexo indica o fecho transitivo de uma relação. Para entender esse operador, suponha que a relação S de dois números naturais sucessores. Seu fecho transitivo seria a união entre os seguintes conjuntos: S U S.S U S.S.S U S.S.S.S U ... Ou seja o fecho transitivo é a relação < (menor que). O operador de "&" é a intercessão de conjuntos. A palavra reservada "no" indica que o conjunto é vazio. Em outras palavras: se o objeto A está relacionado com B, B não está relacionado com A.

A terceira restrição, "(Elem->Elem-iden in ^lessThan + ~(^lessThan))", diz que a relação é acíclica. "Elem->Elem" é a relação de todos os objetos da classe "Elem" com essa mesma classe e é chamada de produto cartesiano. "Elem->Elem-iden" o operador de "-" está retirando do produto cartesiano a relação identidade, ou seja é o produto cartesiano sem elementos que se relacionam consigo mesmo. O operador de "+" é a união de conjuntos.

Um exemplo gerado pelo Alloy é:

Agora que os elementos da classe "Elem" possuem uma relação de sucessor, vamos criar uma classe singleton para modelar ordenação.

sig Elem{
  lessThan: set Elem
}


one sig Sorter{
  toBeSorted : (seq Elem),
  sorted : (seq Elem)
}{
  toBeSorted.elems = Elem
  #toBeSorted.inds = #Elem
}


fact Sorting{
  all i : Sorter.sorted.butlast.inds | 
      Sorter.sorted[i]->Sorter.sorted[i.add[1]] in
      lessThan
}


check{Sorter.toBeSorted.elems = Sorter.sorted.elems}




fact Injective{
  ~lessThan.lessThan in iden
}


fact Asymmetric{
  no ^lessThan & ~(^lessThan)
}


fact Acyclic{
  (Elem->Elem-iden in ^lessThan + ~(^lessThan))
}


run {} for 7

Observe o seguinte trecho de código:

one sig Sorter{
  toBeSorted : (seq Elem),
  sorted : (seq Elem)
}{
  toBeSorted.elems = Elem
  #toBeSorted.inds = #Elem
}


fact Sorting{
  all i : Sorter.sorted.butlast.inds | 
      Sorter.sorted[i]->Sorter.sorted[i.add[1]] in
      lessThan
}


check{Sorter.toBeSorted.elems = Sorter.sorted.elems}

O trecho: "one sig Sorter" indica com a palavra reservada "one" indica que a classe "Sorter" possui um único objeto. As relações "toBeSorted" e "sorted" são as entradas e saídas de um algoritimo de ordenção.

Os trechos "toBeSorted.elems = Elem" e "#toBeSorted.inds = #Elem" Indicam que todos os objetos da classe "Elem" serão ordenados e que cada um deles possui um índice, respectivamente. A restrição "Sorting" indica que a saída é uma sequência ordenada.

Observe a palavra reservada "check" e o que está escrito entre as respectivas chaves. Alloy é capaz de checar se a sequencia de entrada é uma permutação dos elementos de saída.

Então não basta apenas a saída estar ordenada, mas também precisa preservar os elementos de entrada. Observe é essa especificação parece evidente ,mas não é. De fato, Alloy gera um contra-exemplo:

Nesse caso tem-se uma sequencia com um único elemento, e a saída é uma sequencia vazia.

sig Elem{
  lessThan: set Elem
}


one sig Sorter{
  toBeSorted : (seq Elem),
  sorted : (seq Elem)
}{
  toBeSorted.elems = Elem
  #toBeSorted.inds = #Elem
  sorted.elems = Elem //Restrição adicionada
}


fact Sorting{
  all i : Sorter.sorted.butlast.inds | 
      Sorter.sorted[i]->Sorter.sorted[i.add[1]] in
      lessThan
}


check{Sorter.toBeSorted.elems = Sorter.sorted.elems}




fact Injective{
  ~lessThan.lessThan in iden
}


fact Asymmetric{
  no ^lessThan & ~(^lessThan)
}


fact Acyclic{
  (Elem->Elem-iden in ^lessThan + ~(^lessThan))
}


run {} for 7

Ao adicionar a restrição de que a saída é permutação da entrada, Alloy já não gera contra-exemplos.

Próximo artigo, explico sobre problemas em que o design gera modelos incompatíveis com a realidade.